diff -r 9a4b4b7d11d5 -r f6164be9280d src/Tools/isac/Scripts/term_G.sml
--- a/src/Tools/isac/Scripts/term_G.sml	Fri Aug 20 16:37:52 2010 +0200
+++ b/src/Tools/isac/Scripts/term_G.sml	Fri Aug 20 17:02:49 2010 +0200
@@ -6,7 +6,7 @@
 *)
 
 (*
-> (Thm.cterm thy) a_term;
+> (cterm_of thy) a_term;
 val it = "empty" : cterm        *)
 
 (*2003 fun match thy t pat =
@@ -261,7 +261,7 @@
 > val tt = (term_of o the o (parse thy)) "R=(R::real)";
 > val TT = type_of tt;
 > val ss = list2isalist TT [tt,tt,tt];
-> (Thm.cterm thy) ss;
+> (cterm_of thy) ss;
 val it = "[R = R, R = R, R = R]" : cterm  *)
 
 fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
@@ -574,7 +574,7 @@
 (*
 val T =  (type_of o term_of o the) (parse thy "#12::real");
 val t = mk_factroot "SqRoot.sqrt" T 2 3;
-(Thm.cterm thy) t;
+(cterm_of thy) t;
 val it = "#2 * sqrt #3 " : cterm
 *)
 fun var_op_num v op_ optype ntyp n =
@@ -591,7 +591,7 @@
 (*
 > val t = num_op_num "Int" 3 4;
 > atomty t;
-> string_of_cterm ((Thm.cterm thy) t);
+> string_of_cterm ((cterm_of thy) t);
 *)
 
 fun const_in str (Const _) = false
@@ -768,7 +768,7 @@
 atomty t;                         (* 'a *)
 val t' = set_types al t;
 atomty t';                        (*real*)
-(Thm.cterm thy) t';
+(cterm_of thy) t';
 val it = "x = #0 + #-1 * #-4" : cterm
 
 val t = (term_of o the o (parse thy)) 
@@ -776,7 +776,7 @@
 atomty t;
 val t' = set_types al t;
 atomty t';
-(Thm.cterm thy) t';
+(cterm_of thy) t';
 uncaught exception TYPE               (*^^^ is new, NOT in al*)
 *)
       
@@ -1110,7 +1110,7 @@
 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
 val t = Free ("R","?DUMMY") : term
 > val t' = typ_a2real t;
-> (Thm.cterm thy) t';
+> (cterm_of thy) t';
 val it = "R::RealDef.real" : cterm
 
 > val str = "R=R";
@@ -1121,13 +1121,13 @@
 ***   Free ( R, RealDef.real)
 ***   Free ( R, RealDef.real)
 > val t' = typ_a2real t;
-> (Thm.cterm thy) t';
+> (cterm_of thy) t';
 val it = "(R::RealDef.real) = R" : cterm
 
 > val str = "fixed_values [R=R]";
 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
 > val t' = typ_a2real t;
-> (Thm.cterm thy) t';
+> (cterm_of thy) t';
 val it = "fixed_values [(R::RealDef.real) = R]" : cterm
 *)