1.1 --- a/src/Tools/isac/Scripts/term_G.sml	Fri Aug 20 16:37:52 2010 +0200
     1.2 +++ b/src/Tools/isac/Scripts/term_G.sml	Fri Aug 20 17:02:49 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  *)
     1.5  
     1.6  (*
     1.7 -> (Thm.cterm thy) a_term;
     1.8 +> (cterm_of thy) a_term;
     1.9  val it = "empty" : cterm        *)
    1.10  
    1.11  (*2003 fun match thy t pat =
    1.12 @@ -261,7 +261,7 @@
    1.13  > val tt = (term_of o the o (parse thy)) "R=(R::real)";
    1.14  > val TT = type_of tt;
    1.15  > val ss = list2isalist TT [tt,tt,tt];
    1.16 -> (Thm.cterm thy) ss;
    1.17 +> (cterm_of thy) ss;
    1.18  val it = "[R = R, R = R, R = R]" : cterm  *)
    1.19  
    1.20  fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
    1.21 @@ -574,7 +574,7 @@
    1.22  (*
    1.23  val T =  (type_of o term_of o the) (parse thy "#12::real");
    1.24  val t = mk_factroot "SqRoot.sqrt" T 2 3;
    1.25 -(Thm.cterm thy) t;
    1.26 +(cterm_of thy) t;
    1.27  val it = "#2 * sqrt #3 " : cterm
    1.28  *)
    1.29  fun var_op_num v op_ optype ntyp n =
    1.30 @@ -591,7 +591,7 @@
    1.31  (*
    1.32  > val t = num_op_num "Int" 3 4;
    1.33  > atomty t;
    1.34 -> string_of_cterm ((Thm.cterm thy) t);
    1.35 +> string_of_cterm ((cterm_of thy) t);
    1.36  *)
    1.37  
    1.38  fun const_in str (Const _) = false
    1.39 @@ -768,7 +768,7 @@
    1.40  atomty t;                         (* 'a *)
    1.41  val t' = set_types al t;
    1.42  atomty t';                        (*real*)
    1.43 -(Thm.cterm thy) t';
    1.44 +(cterm_of thy) t';
    1.45  val it = "x = #0 + #-1 * #-4" : cterm
    1.46  
    1.47  val t = (term_of o the o (parse thy)) 
    1.48 @@ -776,7 +776,7 @@
    1.49  atomty t;
    1.50  val t' = set_types al t;
    1.51  atomty t';
    1.52 -(Thm.cterm thy) t';
    1.53 +(cterm_of thy) t';
    1.54  uncaught exception TYPE               (*^^^ is new, NOT in al*)
    1.55  *)
    1.56        
    1.57 @@ -1110,7 +1110,7 @@
    1.58  > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
    1.59  val t = Free ("R","?DUMMY") : term
    1.60  > val t' = typ_a2real t;
    1.61 -> (Thm.cterm thy) t';
    1.62 +> (cterm_of thy) t';
    1.63  val it = "R::RealDef.real" : cterm
    1.64  
    1.65  > val str = "R=R";
    1.66 @@ -1121,13 +1121,13 @@
    1.67  ***   Free ( R, RealDef.real)
    1.68  ***   Free ( R, RealDef.real)
    1.69  > val t' = typ_a2real t;
    1.70 -> (Thm.cterm thy) t';
    1.71 +> (cterm_of thy) t';
    1.72  val it = "(R::RealDef.real) = R" : cterm
    1.73  
    1.74  > val str = "fixed_values [R=R]";
    1.75  > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
    1.76  > val t' = typ_a2real t;
    1.77 -> (Thm.cterm thy) t';
    1.78 +> (cterm_of thy) t';
    1.79  val it = "fixed_values [(R::RealDef.real) = R]" : cterm
    1.80  *)
    1.81