1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -137,10 +137,10 @@
     1.4  	   val (f, ts) = strip_comb t and (g, us) = strip_comb u;
     1.5  	   val _=writeln("t= f@ts= \""^
     1.6  	      ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
     1.7 -	      (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
     1.8 +	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
     1.9  	   val _=writeln("u= g@us= \""^
    1.10  	      ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
    1.11 -	      (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
    1.12 +	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
    1.13  	   val _=writeln("size_of_term(t,u)= ("^
    1.14  	      (string_of_int(size_of_term' t))^", "^
    1.15  	      (string_of_int(size_of_term' u))^")");
    1.16 @@ -158,10 +158,10 @@
    1.17  	     end
    1.18  	 | ord => ord)
    1.19  and hd_ord (f, g) =                                        (* ~ term.ML *)
    1.20 -  prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, 
    1.21 +  prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, 
    1.22  						     dest_hd' g)
    1.23  and terms_ord str pr (ts, us) = 
    1.24 -    list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
    1.25 +    list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
    1.26  (**)
    1.27  in
    1.28  (**)
    1.29 @@ -260,7 +260,7 @@
    1.30        erls = Atools_erls, srls = Erls, calc = [],
    1.31        rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
    1.32   	       (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
    1.33 -	       Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}),
    1.34 +	       Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
    1.35   	       (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
    1.36  	       (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
    1.37  	       Rls_ norm_Rational_noadd_fractions(**2**),