1.1 --- a/src/Tools/isac/Scripts/Tools.sml	Fri Aug 20 12:25:37 2010 +0200
     1.2 +++ b/src/Tools/isac/Scripts/Tools.sml	Fri Aug 20 14:58:43 2010 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4   \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\
     1.5   \else hd [A = a * b, a // #2 = #2]";
     1.6  
     1.7 -> cterm_of (sign_of thy) t';
     1.8 +> (Thm.cterm thy) t';
     1.9  > val t = (term_of o the o (parse thy)) s;
    1.10  > val eval_fn = the (assoc (!eval_list, op_));
    1.11  > val (SOME(_,t')) = get_pair op_ eval_fn t;
    1.12 @@ -92,7 +92,7 @@
    1.13  
    1.14  > val eval_fn = the (assoc (!eval_list, op_));
    1.15  > val (SOME(id,t')) = get_pair op_ eval_fn t;
    1.16 -> cterm_of (sign_of thy) t';
    1.17 +> (Thm.cterm thy) t';
    1.18  val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"
    1.19  *)
    1.20