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