1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Mar 10 15:19:26 2011 +0100
1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Thu Mar 10 16:04:00 2011 +0100
1.3 @@ -488,7 +488,7 @@
1.4 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
1.5 val SOME (s',_) = rewrite_set_ thy false list_rls s;
1.6 val s'' = term2str s';
1.7 -if s''="True" then () else error "new behaviour with list_rls 1.2.";
1.8 +if s''="HOL.True" then () else error "new behaviour with list_rls 1.2.";
1.9
1.10 (*--- 2.line in script ---*)
1.11 val t = str2term