1.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Dec 07 10:01:49 2015 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Mon Dec 07 10:17:08 2015 +0100
     1.3 @@ -682,7 +682,7 @@
     1.4  *)
     1.5  
     1.6  fun make_rule thy t =
     1.7 -  let val ct = cterm_of thy (Trueprop $ t)
     1.8 +  let val ct = Thm.global_cterm_of thy (Trueprop $ t)
     1.9    in Thm (term_to_string''' thy (term_of ct), make_thm ct) end;
    1.10  
    1.11  (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;