# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1406127342 -7200
# Node ID 1c66008ca7fb5b12eb1d32d9e83d80f99326c6f7
# Parent  8e3f73e1e3a3a4409cde5e11a60c85a4b6bc2bcc
re-ordered calcelems preparing next changeset

diff -r 8e3f73e1e3a3 -r 1c66008ca7fb src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Wed Jul 23 14:32:19 2014 +0200
+++ b/src/Tools/isac/calcelems.sml	Wed Jul 23 16:55:42 2014 +0200
@@ -203,9 +203,61 @@
      errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
      scr      : scr};      (* Rfuns {...}  (how to restrict type ???)         *)
 
+(*ad thm':
+   there are two kinds of theorems ...
+   (1) known by isabelle
+   (2) not known, eg. calc_thm, instantiated rls
+       the latter have a thmid "#..."
+   and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
+   and have a special assoc_thm / assoc_rls in this interface      *)
+type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
+type domID = string;   (* domID ^".thy" = theory' WN.101011 replace by thyID*)
+type thyID = string;    (*WN.3.11.03 TODO: replace domID with thyID*)
+     
+fun term_to_string' ctxt t =
+  let
+    val ctxt' = Config.put show_markup false ctxt
+  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
+fun term_to_string'' (thyID : thyID) t =
+  let
+    val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
+  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
+fun term_to_string''' thy t =
+  let
+    val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
+  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
+
 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
 
+fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
+fun terms2strs ts = map term2str ts;
+(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
+val terms2str = strs2str o terms2strs;
+(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
+val terms2str' = strs2str' o terms2strs;
+(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
+
+fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
+  | termopt2str NONE = "NONE";
+
+fun type_to_string' ctxt t =
+  let
+    val ctxt' = Config.put show_markup false ctxt
+  in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
+fun type_to_string'' (thyID : thyID) t =
+  let
+    val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
+  in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
+fun type_to_string''' thy t =
+  let
+    val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
+  in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
+
+fun type2str typ = type_to_string'' "Isac" typ; (*legacy*)
+val string_of_typ = type2str; (*legacy*)
+fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
+                 
 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
                                      
 val e_rule = Thm ("refl", @{thm refl});
@@ -283,17 +335,6 @@
 val e_term = Const("empty", Type("'a", []));
 val e_scr = Prog e_term;
 
-(*ad thm':
-   there are two kinds of theorems ...
-   (1) known by isabelle
-   (2) not known, eg. calc_thm, instantiated rls
-       the latter have a thmid "#..."
-   and thus outside isa we ALWAYS transport both (thmid,string_of_thmI)
-   and have a special assoc_thm / assoc_rls in this interface      *)
-type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
-type domID = string;   (* domID ^".thy" = theory' WN.101011 replace by thyID*)
-type thyID = string;    (*WN.3.11.03 TODO: replace domID with thyID*)
-
 fun string_of_thy thy = Context.theory_name thy: theory';
 val theory2domID = string_of_thy;
 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
@@ -715,47 +756,6 @@
   handle _ => error ("ME_Isa: rew_ord '"^ro^"' not in system");
 (*get the string for stac from rule*)
 
-fun term_to_string' ctxt t =
-  let
-    val ctxt' = Config.put show_markup false ctxt
-  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
-fun term_to_string'' (thyID : thyID) t =
-  let
-    val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
-  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
-fun term_to_string''' thy t =
-  let
-    val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
-  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
-
-fun term2str t = term_to_string' (assoc_thy "Isac" |> thy2ctxt) t;
-fun terms2strs ts = map term2str ts;
-(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
-val terms2str = strs2str o terms2strs;
-(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
-val terms2str' = strs2str' o terms2strs;
-(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
-
-fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
-  | termopt2str NONE = "NONE";
-
-fun type_to_string' ctxt t =
-  let
-    val ctxt' = Config.put show_markup false ctxt
-  in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
-fun type_to_string'' (thyID : thyID) t =
-  let
-    val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info.get_theory thyID))
-  in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
-fun type_to_string''' thy t =
-  let
-    val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
-  in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
-
-fun type2str typ = type_to_string'' "Isac" typ; (*legacy*)
-val string_of_typ = type2str; (*legacy*)
-fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
-                 
 fun subst2str (s:subst) =
     (strs2str o
      (map (linefeed o pair2str o