1.1 --- a/src/Tools/isac/Isac_Mathengine.thy	Fri Aug 20 16:21:41 2010 +0200
     1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy	Fri Aug 20 16:37:52 2010 +0200
     1.3 @@ -39,12 +39,8 @@
     1.4  use "ME/calchead.sml"
     1.5  use "ME/appl.sml"
     1.6  use "ME/rewtools.sml"
     1.7 +use "ME/script.sml"
     1.8  
     1.9 -ML {*
    1.10 -PureThy.all_thms_of;
    1.11 -*}
    1.12 -
    1.13 -use "ME/script.sml"
    1.14  
    1.15  ML {*
    1.16  111;

     2.1 --- a/src/Tools/isac/ME/script.sml	Fri Aug 20 16:21:41 2010 +0200
     2.2 +++ b/src/Tools/isac/ME/script.sml	Fri Aug 20 16:37:52 2010 +0200
     2.3 @@ -158,7 +158,8 @@
     2.4  *)
     2.5  
     2.6  fun test_negotiable t = 
     2.7 -    member op = (!negotiable) ((strip_thy o (term_str Script.thy) o head_of) t);
     2.8 +    member op = (!negotiable) 
     2.9 +           ((strip_thy o (term_str (theory "Script")) o head_of) t);
    2.10  
    2.11  (*.get argument of first stactic in a script for init_form.*)
    2.12  fun get_stac thy (h $ body) =
    2.13 @@ -804,10 +805,11 @@
    2.14  *)
    2.15  (* 13.3.01
    2.16  v
    2.17 +string_of_cterm (cterm_of (sign_of " --> "(Syntax.string_of_term (thy2ctxt "
    2.18  *)
    2.19  fun make_rule thy t =
    2.20 -  let val ct = (Thm.cterm thy) (Trueprop $ t)
    2.21 -  in Thm (string_of_cterm ct, make_thm ct) end;
    2.22 +  let val ct = Thm.cterm_of thy (Trueprop $ t)
    2.23 +  in Thm (Syntax.string_of_term (thy2ctxt thy) (term_of ct), make_thm ct) end;
    2.24  
    2.25  (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
    2.26     *)