1.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -93,9 +93,9 @@
     1.4  else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
     1.5  
     1.6  val SOME t = parse thy "solution LL";
     1.7 -atomty (term_of t);
     1.8 +atomty (Thm.term_of t);
     1.9  val SOME t = parse thy "solution LL";
    1.10 -atomty (term_of t);
    1.11 +atomty (Thm.term_of t);
    1.12  
    1.13  val t = str2term 
    1.14  "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
    1.15 @@ -449,7 +449,7 @@
    1.16     *)
    1.17  > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
    1.18  val equalities_es_ = "equalities es_" : string
    1.19 -> val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
    1.20 +> val (dd, ii) = (split_did o Thm.term_of o the o (parse thy)) equalities_es_;
    1.21  > show_types:=true; term2str ii; show_types:=false;
    1.22  val it = "es_::bool list" : string
    1.23  ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~