1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:27:19 2015 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:33:55 2015 +0200
     1.3 @@ -422,20 +422,6 @@
     1.4      else thmid |> convert_metaview_to_thmid thy |> num_str
     1.5    ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) => 
     1.6      error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
     1.7 -(*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
     1.8 -val it = "6 = 2 * 3" : thm          
     1.9 -
    1.10 -> assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");
    1.11 -val it = "0 + ?z = ?z" : thm
    1.12 -
    1.13 -> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
    1.14 -val it = "?t = 0 + ?t"  [.] : thm
    1.15 -
    1.16 -> assoc_thm' @{theory HOL} ("sym_real_add_zero_left","");
    1.17 -*** Unknown theorem(s) "add_0_left"
    1.18 -*** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
    1.19 - uncaught exception ERROR*)
    1.20 -
    1.21  
    1.22  fun parse' (thy:theory') (ct:cterm') =
    1.23      case parse (assoc_thy thy) ct of

     2.1 --- a/src/Tools/isac/calcelems.sml	Mon Apr 20 10:27:19 2015 +0200
     2.2 +++ b/src/Tools/isac/calcelems.sml	Mon Apr 20 10:33:55 2015 +0200
     2.3 @@ -292,6 +292,7 @@
     2.4  
     2.5  (*check for [.] as caused by "fun assoc_thm'"*)
     2.6  fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (prop_of thm)
     2.7 +fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (prop_of thm)
     2.8  fun string_of_thmI thm =
     2.9    let 
    2.10      val str = (de_quote o string_of_thm) thm

     3.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:27:19 2015 +0200
     3.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Mon Apr 20 10:33:55 2015 +0200
     3.3 @@ -21,6 +21,7 @@
     3.4  "----------- fun app_rev, Rrls, -------------------------";
     3.5  "----------- 2011 thms with axclasses -------------------";
     3.6  "----------- repair NO asms from rls RatEq_eliminate ----";
     3.7 +"----------- fun assoc_thm' -----------------------------";
     3.8  "--------------------------------------------------------";
     3.9  "--------------------------------------------------------";
    3.10  "--------------------------------------------------------";
    3.11 @@ -541,3 +542,24 @@
    3.12  trace_rewrite := false;
    3.13  (* WN120317.TODO dropped rateq: the above error is the same in 2002 *)
    3.14  
    3.15 +"----------- fun assoc_thm' -----------------------------";
    3.16 +"----------- fun assoc_thm' -----------------------------";
    3.17 +"----------- fun assoc_thm' -----------------------------";
    3.18 +val thy = @{theory ProgLang}
    3.19 +
    3.20 +val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
    3.21 +if string_of_thm' thy tth = "6 = 2 * 3" then ()
    3.22 +else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
    3.23 +
    3.24 +val tth = assoc_thm' thy ("add_0_left","");
    3.25 +if string_of_thm' thy tth = "0 + ?a = ?a" then ()
    3.26 +else error "assoc_thm' (add_0_left,\"\") changed";
    3.27 +
    3.28 +val tth = assoc_thm' thy ("sym_add_0_left","");
    3.29 +if string_of_thm' thy tth = "?t = 0 + ?t" then ()
    3.30 +else error "assoc_thm' (sym_add_0_left,\"\") changed";
    3.31 +
    3.32 +val tth = assoc_thm' thy ("add_commute","");
    3.33 +if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
    3.34 +else error "assoc_thm' (add_commute,\"\") changed"
    3.35 +