1.1 --- a/test/Tools/isac/Knowledge/polyeq.sml	Thu Mar 10 15:19:26 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml	Thu Mar 10 16:04:00 2011 +0100
     1.3 @@ -46,54 +46,54 @@
     1.4  
     1.5   val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
     1.6   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
     1.7 - if (term2str t) = "True" then ()
     1.8 + if (term2str t) = "HOL.True" then ()
     1.9   else  error "polyeq.sml: diff.behav. 1 in is_expended_in";
    1.10  
    1.11   val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
    1.12   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
    1.13 - if (term2str t) = "False" then ()
    1.14 + if (term2str t) = "HOL.False" then ()
    1.15   else  error "polyeq.sml: diff.behav. 2 in is_poly_in";
    1.16  
    1.17  
    1.18   val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
    1.19   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
    1.20 - if (term2str t) = "True" then ()
    1.21 + if (term2str t) = "HOL.True" then ()
    1.22   else  error "polyeq.sml: diff.behav. 3 in is_poly_in";
    1.23  
    1.24  
    1.25   val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
    1.26   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
    1.27 - if (term2str t) = "True" then ()
    1.28 + if (term2str t) = "HOL.True" then ()
    1.29   else  error "polyeq.sml: diff.behav. 4 in is_expended_in";
    1.30  
    1.31  
    1.32   val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
    1.33   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
    1.34 - if (term2str t) = "True" then ()
    1.35 + if (term2str t) = "HOL.True" then ()
    1.36   else  error "polyeq.sml: diff.behav. 5 in is_expended_in";
    1.37   
    1.38   val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
    1.39   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
    1.40 - if (term2str t) = "True" then ()
    1.41 + if (term2str t) = "HOL.True" then ()
    1.42   else  error "polyeq.sml: diff.behav. in has_degree_in_in";
    1.43  
    1.44  
    1.45   val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
    1.46   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
    1.47 - if (term2str t) = "False" then ()
    1.48 + if (term2str t) = "HOL.False" then ()
    1.49   else  error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
    1.50  
    1.51   val t4 = (term_of o the o (parse thy)) 
    1.52  	      "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
    1.53   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
    1.54 - if (term2str t) = "False" then ()
    1.55 + if (term2str t) = "HOL.False" then ()
    1.56   else  error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
    1.57  
    1.58  
    1.59   val t5 = (term_of o the o (parse thy)) 
    1.60  	      "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
    1.61   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
    1.62 - if (term2str t) = "True" then ()
    1.63 + if (term2str t) = "HOL.True" then ()
    1.64   else  error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
    1.65  
    1.66  
    1.67 @@ -848,7 +848,7 @@
    1.68   val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
    1.69   val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
    1.70   val t' = term2str t;
    1.71 - (*if t'= "True" then ()
    1.72 + (*if t'= "HOL.True" then ()
    1.73   else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
    1.74  (* *)
    1.75   val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",