1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Mon Dec 07 10:01:49 2015 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Mon Dec 07 10:17:08 2015 +0100
     1.3 @@ -323,7 +323,7 @@
     1.4  	val t' = case t of
     1.5  		     Const ("==>",_) $ _ $ _ => t
     1.6  		   | _ => Trueprop $ t
     1.7 -    in make_thm (cterm_of thy t') end;
     1.8 +    in make_thm (Thm.global_cterm_of thy t') end;
     1.9  (*
    1.10    val str = "?r ^^^ 2 = ?r * ?r";
    1.11    val thm = realpow_twoI;
    1.12 @@ -355,7 +355,7 @@
    1.13  (*prints subgoal etc. 
    1.14  ((goal thy);(topthm()) o ) str;                      *)
    1.15  (*assume rejects scheme variables 
    1.16 -  assume ((cterm_of thy) (Trueprop $ 
    1.17 +  assume ((Thm.global_cterm_of thy) (Trueprop $ 
    1.18  		(term_of o the o (parse thy)) str)); *)
    1.19  
    1.20