1.1 --- a/src/Tools/isac/Interpret/appl.sml	Thu Mar 10 15:19:26 2011 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Thu Mar 10 16:04:00 2011 +0100
     1.3 @@ -165,12 +165,12 @@
     1.4  > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
     1.5  	   \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
     1.6  > val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
     1.7 -val ct' = "True" : cterm'
     1.8 +val ct' = "HOL.True" : cterm'
     1.9  
    1.10  > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
    1.11  	   \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
    1.12  > val SOME(ct',_) = rewrite_set "Isac"  false "eval_rls" ct;
    1.13 -val ct' = "True" : cterm'
    1.14 +val ct' = "HOL.True" : cterm'
    1.15  
    1.16  
    1.17  > val const  = (term_of o the o (parse thy)) "(#3::real)";