# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1282315072 -7200
# Node ID 9a4b4b7d11d533ab5989369fd7c1e65f4cf41fb0
# Parent  8de0b6207074d447d2667df9095bbb4788cc373f
updated ME/script.sml

found wrong replacement --> (Thm.cterm thy) in subsequent thys

diff -r 8de0b6207074 -r 9a4b4b7d11d5 src/Tools/isac/Isac_Mathengine.thy
--- a/src/Tools/isac/Isac_Mathengine.thy	Fri Aug 20 16:21:41 2010 +0200
+++ b/src/Tools/isac/Isac_Mathengine.thy	Fri Aug 20 16:37:52 2010 +0200
@@ -39,12 +39,8 @@
 use "ME/calchead.sml"
 use "ME/appl.sml"
 use "ME/rewtools.sml"
+use "ME/script.sml"
 
-ML {*
-PureThy.all_thms_of;
-*}
-
-use "ME/script.sml"
 
 ML {*
 111;
diff -r 8de0b6207074 -r 9a4b4b7d11d5 src/Tools/isac/ME/script.sml
--- a/src/Tools/isac/ME/script.sml	Fri Aug 20 16:21:41 2010 +0200
+++ b/src/Tools/isac/ME/script.sml	Fri Aug 20 16:37:52 2010 +0200
@@ -158,7 +158,8 @@
 *)
 
 fun test_negotiable t = 
-    member op = (!negotiable) ((strip_thy o (term_str Script.thy) o head_of) t);
+    member op = (!negotiable) 
+           ((strip_thy o (term_str (theory "Script")) o head_of) t);
 
 (*.get argument of first stactic in a script for init_form.*)
 fun get_stac thy (h $ body) =
@@ -804,10 +805,11 @@
 *)
 (* 13.3.01
 v
+string_of_cterm (cterm_of (sign_of " --> "(Syntax.string_of_term (thy2ctxt "
 *)
 fun make_rule thy t =
-  let val ct = (Thm.cterm thy) (Trueprop $ t)
-  in Thm (string_of_cterm ct, make_thm ct) end;
+  let val ct = Thm.cterm_of thy (Trueprop $ t)
+  in Thm (Syntax.string_of_term (thy2ctxt thy) (term_of ct), make_thm ct) end;
 
 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
    *)