<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
<HTML>
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=us-ascii">
<META NAME="Generator" CONTENT="MS Exchange Server version 5.5.2657.73">
<TITLE>Re: Type-check bug? -- final character</TITLE>
</HEAD>
<BODY>
<P><FONT SIZE=2>Oops. Because of an editing error, I left off the final character -- but only the final character -- of the problem example. It should have been the following:</FONT></P>
<P><FONT SIZE=2>new_theory "test";</FONT>
<BR><FONT SIZE=2>set_flag ("z_type_check_only", false);</FONT>
<BR><FONT SIZE=2>%SZS% S1 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%</FONT>
<BR><FONT SIZE=2>%BV% x1: TV1;</FONT>
<BR><FONT SIZE=2>%BV% x2: %bbP% TV2</FONT>
<BR><FONT SIZE=2>^</FONT>
<BR><FONT SIZE=2>%SZS% S2 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%</FONT>
<BR><FONT SIZE=2>%BV% x3: %bbP% S1</FONT>
<BR><FONT SIZE=2>^</FONT>
<BR><FONT SIZE=2>%SZS% S3 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%</FONT>
<BR><FONT SIZE=2>%BV% x4: %bbP% S2</FONT>
<BR><FONT SIZE=2>^</FONT>
</P>
<P><FONT SIZE=2>Steve</FONT>
</P>
</BODY>
</HTML>