# HG changeset patch
# User Walther Neuper <wneuper@ist.tugraz.at>
# Date 1429518835 -7200
# Node ID 57739650f9b4f5cea9ee7f2d781d972ddee8e2b9
# Parent  b42e334c97eed2074c3aff5a70287e3d2a450fcc
Build_Isac.thy WORKS: shift new tests from "src" to "test"

Note: the other tests do not yet run; they will be reviewed with
"isabelle jedit -l Isac"

diff -r b42e334c97ee -r 57739650f9b4 src/Tools/isac/ProgLang/rewrite.sml
--- a/src/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:27:19 2015 +0200
+++ b/src/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:33:55 2015 +0200
@@ -422,20 +422,6 @@
     else thmid |> convert_metaview_to_thmid thy |> num_str
   ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) => 
     error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
-(*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
-val it = "6 = 2 * 3" : thm          
-
-> assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");
-val it = "0 + ?z = ?z" : thm
-
-> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
-val it = "?t = 0 + ?t"  [.] : thm
-
-> assoc_thm' @{theory HOL} ("sym_real_add_zero_left","");
-*** Unknown theorem(s) "add_0_left"
-*** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
- uncaught exception ERROR*)
-
 
 fun parse' (thy:theory') (ct:cterm') =
     case parse (assoc_thy thy) ct of
diff -r b42e334c97ee -r 57739650f9b4 src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Mon Apr 20 10:27:19 2015 +0200
+++ b/src/Tools/isac/calcelems.sml	Mon Apr 20 10:33:55 2015 +0200
@@ -292,6 +292,7 @@
 
 (*check for [.] as caused by "fun assoc_thm'"*)
 fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (prop_of thm)
+fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (prop_of thm)
 fun string_of_thmI thm =
   let 
     val str = (de_quote o string_of_thm) thm
diff -r b42e334c97ee -r 57739650f9b4 test/Tools/isac/ProgLang/rewrite.sml
--- a/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:27:19 2015 +0200
+++ b/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:33:55 2015 +0200
@@ -21,6 +21,7 @@
 "----------- fun app_rev, Rrls, -------------------------";
 "----------- 2011 thms with axclasses -------------------";
 "----------- repair NO asms from rls RatEq_eliminate ----";
+"----------- fun assoc_thm' -----------------------------";
 "--------------------------------------------------------";
 "--------------------------------------------------------";
 "--------------------------------------------------------";
@@ -541,3 +542,24 @@
 trace_rewrite := false;
 (* WN120317.TODO dropped rateq: the above error is the same in 2002 *)
 
+"----------- fun assoc_thm' -----------------------------";
+"----------- fun assoc_thm' -----------------------------";
+"----------- fun assoc_thm' -----------------------------";
+val thy = @{theory ProgLang}
+
+val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
+if string_of_thm' thy tth = "6 = 2 * 3" then ()
+else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
+
+val tth = assoc_thm' thy ("add_0_left","");
+if string_of_thm' thy tth = "0 + ?a = ?a" then ()
+else error "assoc_thm' (add_0_left,\"\") changed";
+
+val tth = assoc_thm' thy ("sym_add_0_left","");
+if string_of_thm' thy tth = "?t = 0 + ?t" then ()
+else error "assoc_thm' (sym_add_0_left,\"\") changed";
+
+val tth = assoc_thm' thy ("add_commute","");
+if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
+else error "assoc_thm' (add_commute,\"\") changed"
+