1.1 --- a/TODO.md	Wed Aug 11 11:54:07 2021 +0200
     1.2 +++ b/TODO.md	Sat Aug 14 13:52:23 2021 +0200
     1.3 @@ -45,6 +45,12 @@
     1.4      ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close>
     1.5  
     1.6  * WN: Avoid Thm.get_name_hint --- somewhat fragile.
     1.7 +    Thm.get_name_hint supports lazyness of students, who do not care about theories
     1.8 +    a theorem is defined in.
     1.9 +    Dropping it, e.g. in "fun revert_sym_rule", breaks tests on Thy_Write.thydata,
    1.10 +    which shall be dropped; see e587c45cae0f note in Build_Thydata.thy.
    1.11 +  + what remains TODO: use Global_Theory.get_thm instead, get theory from References.T
    1.12 +    and push theory through as argument of respective functions.
    1.13  
    1.14  * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
    1.15      - quite often "axiomatization ..." can be turned into "lemma ... by auto"
    1.16 @@ -71,4 +77,4 @@
    1.17  
    1.18  * WN: push suggestions of MW through the whole code
    1.19    + e1da148725ed : \<^ML>\<open>...\<close> instead of parentheses
    1.20 -  + 
    1.21 \ No newline at end of file
    1.22 +  + 

     2.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml	Wed Aug 11 11:54:07 2021 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml	Sat Aug 14 13:52:23 2021 +0200
     2.3 @@ -59,7 +59,7 @@
     2.4  datatype rule =
     2.5      Erule             (* the empty rule                                               *)
     2.6    | Thm of            (* theorem associated with the identifier for reflection        *)
     2.7 -      string *        (* needless since Thm.get_name_hint                             *)
     2.8 +      string *        (* required for ThmC.sym_thm                                    *)
     2.9          Thm.thm       (* see TODO CLEANUP Thm                                         *)
    2.10    | Eval of           (* evaluation by rewriting                                      *)
    2.11        string *        (* unique identifier for the evaluation function                *)

     3.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Wed Aug 11 11:54:07 2021 +0200
     3.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Sat Aug 14 13:52:23 2021 +0200
     3.3 @@ -21,7 +21,7 @@
     3.4    val member': id list -> Rule.rule -> bool
     3.5  
     3.6    val is_sym: id -> bool
     3.7 -  val thm_from_thy: theory -> ThmC_Def.id -> thm
     3.8 +  val thm_from_thy: theory -> id -> thm
     3.9  
    3.10    val revert_sym_rule: theory -> Rule.rule -> Rule.rule
    3.11  
    3.12 @@ -144,15 +144,17 @@
    3.13    | make_sym_rule (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
    3.14    | make_sym_rule r = raise ERROR ("make_sym_rule: not for " ^  Rule.to_string r)
    3.15  
    3.16 +(* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *)
    3.17  fun revert_sym_rule thy (Rule.Thm (id, thm)) =
    3.18 +                            (*this ^^ might come from the user, who doesn't care about thy*)
    3.19        if is_sym (cut_id id)
    3.20        then 
    3.21          let 
    3.22            val id' = id_drop_sym id
    3.23            val thm' = thm_from_thy thy id'
    3.24 -          val id'' = Thm.get_name_hint thm'
    3.25 +          val id'' = Thm.get_name_hint thm'      (*recover the thy the thm comes from*)
    3.26          in Rule.Thm (id'', thm') end
    3.27 -      else Rule.Thm (Thm.get_name_hint thm, thm)
    3.28 +      else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*)
    3.29    | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)
    3.30  
    3.31