1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml	Wed Apr 08 16:56:47 2020 +0200
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml	Thu Apr 09 11:21:53 2020 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
     1.5      XML.Elem (("MESSAGE", []), [XML.Text e])])
     1.6  
     1.7 -fun fetchproposedtacticOK2xml (calcid : Celem.calcID) tac (errpatIDs : Rule.errpatID list) =
     1.8 +fun fetchproposedtacticOK2xml (calcid : Celem.calcID) tac (errpatIDs : Error_Fill_Def.errpatID list) =
     1.9    XML.Elem (("NEXTTAC", []), [
    1.10      XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
    1.11      XML.Elem (("TACTICERRORPATTERNS", []), [xml_of_strs errpatIDs]),

     2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml	Wed Apr 08 16:56:47 2020 +0200
     2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml	Thu Apr 09 11:21:53 2020 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4      val DEconstrCalcTree : Celem.calcID -> XML.tree
     2.5      val fetchApplicableTactics : Celem.calcID -> int -> Pos.pos' -> XML.tree
     2.6      val fetchProposedTactic : Celem.calcID -> XML.tree
     2.7 -    val findFillpatterns : Celem.calcID -> Rule.errpatID -> XML.tree
     2.8 +    val findFillpatterns : Celem.calcID -> Error_Fill_Def.errpatID -> XML.tree
     2.9      val getAccumulatedAsms : Celem.calcID -> Pos.pos' -> XML.tree
    2.10      val getActiveFormula : Celem.calcID -> XML.tree
    2.11      val getAssumptions : Celem.calcID -> Pos.pos' -> XML.tree
    2.12 @@ -49,7 +49,7 @@
    2.13      val refFormula : Celem.calcID -> Pos.pos' -> XML.tree
    2.14      val refineProblem : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
    2.15      val replaceFormula : Celem.calcID -> Rule.cterm' -> XML.tree
    2.16 -    val requestFillformula : Celem.calcID -> Rule.errpatID * Celem.fillpatID -> XML.tree
    2.17 +    val requestFillformula : Celem.calcID -> Error_Fill_Def.errpatID * Error_Fill_Def.fillpatID -> XML.tree
    2.18      val resetCalcHead : Celem.calcID -> XML.tree
    2.19      val setContext : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
    2.20      val setMethod : Celem.calcID -> Celem.metID -> XML.tree
    2.21 @@ -164,7 +164,7 @@
    2.22    	  let
    2.23    	    val _= upd_tacis cI tacis
    2.24    	    val (tac, _, _) = last_elem tacis
    2.25 -  	  in fetchproposedtacticOK2xml cI tac (Error_Pattern.fetchErrorpatterns tac) end
    2.26 +  	  in fetchproposedtacticOK2xml cI tac (Error_Fill_Pattern.fetchErrorpatterns tac) end
    2.27  	| ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
    2.28  	| ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
    2.29  	| ("end-of-calculation", _) =>
    2.30 @@ -660,7 +660,7 @@
    2.31    let
    2.32      val ((pt, _), _) = get_calc cI
    2.33  		val pos = get_pos cI 1;
    2.34 -		val fillpats = Error_Pattern.find_fillpatterns (pt, pos) errpatID
    2.35 +		val fillpats = Error_Fill_Pattern.find_fillpatterns (pt, pos) errpatID
    2.36    in findFillpatterns2xml cI (map #1 fillpats) end
    2.37  
    2.38  (* given a fillpatID propose a fillform to the learner on the worksheet;
    2.39 @@ -673,10 +673,10 @@
    2.40    let
    2.41      val ((pt, _), _) = get_calc cI
    2.42  		val pos = get_pos cI 1
    2.43 -    val fillforms = Error_Pattern.find_fillpatterns (pt, pos) errpatID
    2.44 +    val fillforms = Error_Fill_Pattern.find_fillpatterns (pt, pos) errpatID
    2.45    in
    2.46      case filter ((curry op = fillpatID) o
    2.47 -        (#1: (Celem.fillpatID * term * thm * (Selem.subs option) -> Celem.fillpatID))) fillforms of
    2.48 +        (#1: (Error_Fill_Def.fillpatID * term * thm * (Selem.subs option) -> Error_Fill_Def.fillpatID))) fillforms of
    2.49        (_, fillform, thm, sube_opt) :: _ =>
    2.50          let
    2.51            val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, Celem.thm''_of_thm thm)
    2.52 @@ -697,7 +697,7 @@
    2.53      val ((pt, _), _) = get_calc cI
    2.54      val pos = get_pos cI 1;
    2.55    in
    2.56 -    case Error_Pattern.is_exactly_equal (pt, pos) ifo of
    2.57 +    case Error_Fill_Pattern.is_exactly_equal (pt, pos) ifo of
    2.58        ("ok", tac) =>
    2.59          let
    2.60          in (* cp from applyTactic *)

     3.1 --- a/src/Tools/isac/Build_Isac.thy	Wed Apr 08 16:56:47 2020 +0200
     3.2 +++ b/src/Tools/isac/Build_Isac.thy	Thu Apr 09 11:21:53 2020 +0200
     3.3 @@ -17,7 +17,11 @@
     3.4        ML_file libraryC.sml
     3.5        ML_file "rule-def.sml"
     3.6        ML_file "exec-def.sml"
     3.7 +      ML_file "rewrite-order.sml"
     3.8 +      ML_file theoryC.sml
     3.9        ML_file rule.sml
    3.10 +      ML_file thmC.sml
    3.11 +      ML_file "error-fill-def.sml"
    3.12        ML_file "rule-set.sml"
    3.13        ML_file calcelems.sml
    3.14    theory CalcElements imports KEStore

     4.1 --- a/src/Tools/isac/CalcElements/KEStore.thy	Wed Apr 08 16:56:47 2020 +0200
     4.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy	Thu Apr 09 11:21:53 2020 +0200
     4.3 @@ -11,6 +11,8 @@
     4.4  ML_file "rewrite-order.sml"
     4.5  ML_file theoryC.sml
     4.6  ML_file rule.sml
     4.7 +ML_file thmC.sml
     4.8 +ML_file "error-fill-def.sml"
     4.9  ML_file "rule-set.sml"
    4.10  ML_file calcelems.sml
    4.11  ML \<open>
    4.12 @@ -46,7 +48,7 @@
    4.13    val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
    4.14    val get_thes: theory -> (Celem.thydata Celem.ptyp) list
    4.15    val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    4.16 -  val insert_fillpats: (Celem.theID * Celem.fillpat list) list -> theory -> theory 
    4.17 +  val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    4.18    val get_ref_thy: unit -> theory
    4.19    val set_ref_thy: theory -> unit
    4.20  end;                               

     5.1 --- a/src/Tools/isac/CalcElements/calcelems.sml	Wed Apr 08 16:56:47 2020 +0200
     5.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml	Thu Apr 09 11:21:53 2020 +0200
     5.3 @@ -22,12 +22,15 @@
     5.4      type authors
     5.5      type guh
     5.6  
     5.7 +(*/------- to Error_Fill_Def -------\* )
     5.8      type fillpat
     5.9 +    eqtype fillpatID
    5.10 +( *\------- to Error_Fill_Def -------/*)
    5.11      datatype thydata
    5.12        = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: guh, mathauthors: authors}
    5.13        | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool}
    5.14        | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: ThyC.thyID * Rule_Set.T}
    5.15 -      | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}
    5.16 +      | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: guh, mathauthors: authors, thm: thm}
    5.17        | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
    5.18      type theID
    5.19      type spec
    5.20 @@ -41,7 +44,7 @@
    5.21      val check_metguh_unique: guh -> met ptyp list -> unit
    5.22      val add_thydata: string list * string list -> thydata -> thydata ptyp list -> thydata ptyp list
    5.23      val get_py: 'a ptyp list -> pblID -> string list -> 'a
    5.24 -    val update_hthm: thydata -> fillpat list -> thydata
    5.25 +    val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
    5.26      val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
    5.27      val part2guh: theID -> guh
    5.28      val spec2str: string * string list * string list -> string
    5.29 @@ -81,7 +84,6 @@
    5.30      val thmID_of_derivation_name: string -> string
    5.31      val rls2guh: string * ThyC.thyID -> Rule_Set.identifier -> guh
    5.32      val theID2guh: theID -> guh
    5.33 -    eqtype fillpatID
    5.34      type pbt_ = string * (term * term)
    5.35      eqtype xml
    5.36      val cal2guh: string * ThyC.thyID -> string -> guh
    5.37 @@ -93,14 +95,14 @@
    5.38      val thy2guh: theID -> guh
    5.39      val thypart2guh: theID -> guh
    5.40      val ord2guh: string * ThyC.theory' -> string -> string
    5.41 -    val update_hrls: thydata -> Rule.errpatID list -> thydata
    5.42 +    val update_hrls: thydata -> Error_Fill_Def.errpatID list -> thydata
    5.43      eqtype iterID
    5.44      eqtype calcID
    5.45      val thm''_of_thm: thm -> thm''
    5.46      val thm_of_thm: Rule.rule -> thm
    5.47  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    5.48      val pats2str' : pat list -> string
    5.49 -    val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
    5.50 +    val insert_fillpats: thydata ptyp list -> (pblID * Error_Fill_Def.fillpat list) list -> thydata ptyp list ->
    5.51        thydata ptyp list
    5.52  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    5.53      val knowthys: unit -> theory list
    5.54 @@ -125,7 +127,7 @@
    5.55  
    5.56  (* TODO CLEANUP Thm:
    5.57  Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
    5.58 -                   (b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI
    5.59 +                   (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC.string_of_thmI
    5.60  thmID            : type for data from user input + program
    5.61  thmDeriv         : type for thy_hierarchy ONLY
    5.62  obsolete types   : thm' (SEE "ad thm'"), thm''. 
    5.63 @@ -166,6 +168,7 @@
    5.64  type xml = string; (* rm together with old code replaced by XML.tree *)
    5.65  
    5.66  
    5.67 +(*/------- to Error_Fill_Def -------\* )
    5.68  (* for (at least) 2 kinds of access:
    5.69    (1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats)
    5.70    (2) given a thm, find respective fillpats *)
    5.71 @@ -173,8 +176,9 @@
    5.72  type fillpat =
    5.73    fillpatID   (* DESIGN ?TODO: give an order w.r.t difficulty ? *)
    5.74    * term      (* the pattern with fill-in gaps                  *)
    5.75 -  * Rule.errpatID; (* which the fillpat would be a help for          
    5.76 +  * Error_Fill_Def.errpatID; (* which the fillpat would be a help for          
    5.77                   DESIGN ?TODO: list for several patterns ?      *)
    5.78 +( *\------- to Error_Fill_Def -------/*)
    5.79  
    5.80  
    5.81  (*  WN0509 discussion:
    5.82 @@ -283,7 +287,7 @@
    5.83  (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
    5.84  datatype thydata =
    5.85    Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}
    5.86 -| Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list,
    5.87 +| Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
    5.88     thm: thm} (* here no sym_thm, thus no thmID required *)
    5.89  | Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.thyID * Rule_Set.T)}
    5.90  | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
    5.91 @@ -549,7 +553,7 @@
    5.92        srls       : Rule_Set.T,        (* for evaluating list expressions in scr        *)
    5.93        crls       : Rule_Set.T,        (* for check_elementwise, ie. formulae in calc.  *)
    5.94        nrls       : Rule_Set.T,        (* canonical simplifier specific for this met    *)
    5.95 -      errpats    : Rule.errpat list,(* error patterns expected in this method        *)
    5.96 +      errpats    : Error_Fill_Def.errpat list,(* error patterns expected in this method        *)
    5.97        calc       : Rule_Def.calc list, (* Theory_Data in fun prep_met                   *)
    5.98        (*branch   : TransitiveB set in append_problem at generation ob pblobj         *)
    5.99        scr        : Rule.program,    (* progam, empty as @{thm refl} or Rfuns         *)

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/isac/CalcElements/error-fill-def.sml	Thu Apr 09 11:21:53 2020 +0200
     6.3 @@ -0,0 +1,49 @@
     6.4 +(* Title:  CalcElements/error-pattern-def.sml
     6.5 +   Author: Walther Neuper
     6.6 +   (c) due to copyright terms
     6.7 +
     6.8 +ODO: use "Error_Fill_Def" for renaming identifiers -- go back to Rule_Def.*
     6.9 +*)
    6.10 +signature ERROR_FILL_PATTERN_DEFINITION =
    6.11 +sig
    6.12 +  eqtype errpatID
    6.13 +  type errpat = errpatID * term list * thm list
    6.14 +  val errpats2str : errpat list -> string
    6.15 +  type fillpatID
    6.16 +  type fillpat
    6.17 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    6.18 +  (*NONE*)
    6.19 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    6.20 +  (*NONE*)
    6.21 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    6.22 +end
    6.23 +
    6.24 +(**)
    6.25 +structure Error_Fill_Def(**): ERROR_FILL_PATTERN_DEFINITION(**) =
    6.26 +struct
    6.27 +(**)
    6.28 +
    6.29 +type errpatID = Rule_Def.errpatID
    6.30 +
    6.31 +type errpat =
    6.32 +  errpatID    (* one identifier for a list of patterns                       
    6.33 +                 DESIGN ?TODO: errpatID list for hierarchy of errpats ?      *)
    6.34 +  * term list (* error patterns                                              *)
    6.35 +  * thm list  (* thms related to error patterns; note that respective lhs 
    6.36 +                 do not match (which reflects student's error).
    6.37 +                 fillpatterns are stored with these thms.                    *)
    6.38 +fun errpat2str (id, tms, thms) =
    6.39 +  "(\"" ^ id ^ "\",\n" ^ Rule.terms2str tms ^ ",\n" ^ ThmC.thms2str thms
    6.40 +fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
    6.41 +
    6.42 +(* for (at least) 2 kinds of access:
    6.43 +  (1) given an errpatID, find the respective fillpats (e.g. in fun find_fill_pats)
    6.44 +  (2) given a thm, find respective fillpats *)
    6.45 +type fillpatID = string
    6.46 +type fillpat =
    6.47 +  fillpatID   (* DESIGN ?TODO: give an order w.r.t difficulty ? *)
    6.48 +  * term      (* the pattern with fill-in gaps                  *)
    6.49 +  * errpatID; (* which the fillpat would be a help for          
    6.50 +                 DESIGN ?TODO: list for several patterns ?      *)
    6.51 +
    6.52 +(**)end(**)

     7.1 --- a/src/Tools/isac/CalcElements/rule-set.sml	Wed Apr 08 16:56:47 2020 +0200
     7.2 +++ b/src/Tools/isac/CalcElements/rule-set.sml	Thu Apr 09 11:21:53 2020 +0200
     7.3 @@ -165,7 +165,7 @@
     7.4    | eq_rule _ = false;
     7.5  
     7.6  fun rule2str Rule_Def.Erule = "Erule" 
     7.7 -  | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ Rule.string_of_thmI thm ^ ")"
     7.8 +  | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC.string_of_thmI thm ^ ")"
     7.9    | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
    7.10    | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
    7.11    | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";

     8.1 --- a/src/Tools/isac/CalcElements/rule.sml	Wed Apr 08 16:56:47 2020 +0200
     8.2 +++ b/src/Tools/isac/CalcElements/rule.sml	Thu Apr 09 11:21:53 2020 +0200
     8.3 @@ -2,6 +2,7 @@
     8.4     Author: Walther Neuper 2018
     8.5     (c) copyright due to lincense terms
     8.6  
     8.7 +TODO: use "Rule" for renaming identifiers.
     8.8  Some stuff waits for later rounds of restructuring, e.g. Rule.e_term
     8.9  *)
    8.10  
    8.11 @@ -13,9 +14,6 @@
    8.12    eqtype cterm'
    8.13    type subst = (term * term) list
    8.14  
    8.15 -  eqtype errpatID
    8.16 -  type errpat = errpatID * term list * thm list
    8.17 -
    8.18    val scr2str: program -> string
    8.19  
    8.20    val e_term: term                                           (* shift up to Unparse *)
    8.21 @@ -35,13 +33,8 @@
    8.22  
    8.23  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    8.24    val terms2str': term list -> string                        (* shift up to Unparse *)
    8.25 -  val thm2str: thm -> string
    8.26 -  val thms2str : thm list -> string
    8.27 -  val string_of_thmI: thm -> string
    8.28 -  val string_of_thm': theory -> thm -> string                (* shift up to Unparse *)
    8.29 -  val errpats2str : errpat list -> string
    8.30  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    8.31 -    val string_of_thm: thm -> string                           (* shift up to Unparse *)
    8.32 +  (*NONE*)
    8.33  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    8.34  end
    8.35  
    8.36 @@ -88,28 +81,6 @@
    8.37  fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
    8.38    | termopt2str NONE = "NONE";
    8.39  
    8.40 -fun thm2str thm =
    8.41 -  let
    8.42 -    val t = Thm.prop_of thm
    8.43 -    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
    8.44 -    val ctxt' = Config.put show_markup false ctxt
    8.45 -  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
    8.46 -fun thms2str thms = (strs2str o (map thm2str)) thms
    8.47 -                 
    8.48 -(* error patterns and fill patterns *)
    8.49 -type errpatID = string
    8.50 -type errpat =
    8.51 -  errpatID    (* one identifier for a list of patterns                       
    8.52 -                 DESIGN ?TODO: errpatID list for hierarchy of errpats ?      *)
    8.53 -  * term list (* error patterns                                              *)
    8.54 -  * thm list  (* thms related to error patterns; note that respective lhs 
    8.55 -                 do not match (which reflects student's error).
    8.56 -                 fillpatterns are stored with these thms.                    *)
    8.57 -fun errpat2str (id, tms, thms) =
    8.58 -  "(\"" ^ id ^ "\",\n" ^ terms2str tms ^ ",\n" ^ thms2str thms
    8.59 -fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
    8.60 -
    8.61 -
    8.62  fun type_to_string'' (thyID : ThyC.thyID) t =
    8.63    let
    8.64      val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))
    8.65 @@ -118,19 +89,6 @@
    8.66  val string_of_typ = type2str; (*legacy*)
    8.67  fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
    8.68  
    8.69 -(*check for [.] as caused by "fun assoc_thm'"*)
    8.70 -fun string_of_thm thm = term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
    8.71 -fun string_of_thm' thy thm = term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm)
    8.72 -fun string_of_thmI thm =
    8.73 -  let 
    8.74 -    val str = (de_quote o string_of_thm) thm
    8.75 -    val (a, b) = split_nlast (5, Symbol.explode str)
    8.76 -  in 
    8.77 -    case b of
    8.78 -      [" ", " ","[", ".", "]"] => implode a
    8.79 -    | _ => str
    8.80 -  end
    8.81 -
    8.82  fun scr2str EmptyScr = "EmptyScr"
    8.83    | scr2str (Prog s) = "Prog " ^ term2str s
    8.84    | scr2str (Rfuns _)  = "Rfuns";

     9.1 --- a/src/Tools/isac/CalcElements/theoryC.sml	Wed Apr 08 16:56:47 2020 +0200
     9.2 +++ b/src/Tools/isac/CalcElements/theoryC.sml	Thu Apr 09 11:21:53 2020 +0200
     9.3 @@ -7,7 +7,6 @@
     9.4  *)
     9.5  signature THEORY_ISAC =
     9.6  sig
     9.7 -(*datatype T = Rule_Def.Thm  ..ERROR: cannot get out from Rule_Def.rule*)
     9.8    eqtype thyID
     9.9    eqtype domID
    9.10    eqtype theory'
    9.11 @@ -31,8 +30,6 @@
    9.12  struct
    9.13  (**)
    9.14  
    9.15 -(*datatype T = Rule_Def.Thm  ..ERROR: cannot get out from Rule_Def.rule*)
    9.16 -
    9.17  (* Since Isabelle2017 sessions in theory identifiers are enforced.
    9.18    However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
    9.19  fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
    9.20 @@ -44,7 +41,7 @@
    9.21     (1) known by isabelle
    9.22     (2) not known, eg. calc_thm, instantiated rls
    9.23         the latter have a thmid "#..."
    9.24 -   and thus outside isa we ALWAYS transport both (thmID, string_of_thmI)
    9.25 +   and thus outside isa we ALWAYS transport both (thmID, ThmC.string_of_thmI)
    9.26     and have a special assoc_thm / assoc_rls in this interface      *)
    9.27  type thyID = string;   (* WN.3.11.03 TODO: replace domID with thyID*)
    9.28  type domID = string;   (* domID ^".thy" = theory' WN.101011 replace by thyID*)
    9.29 @@ -59,4 +56,4 @@
    9.30  fun thyID2theory' (thyID:thyID) = thyID;
    9.31  fun theory'2thyID (theory':theory') = theory';
    9.32  
    9.33 -end
    9.34 +(**)end(**)

    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/isac/CalcElements/thmC.sml	Thu Apr 09 11:21:53 2020 +0200
    10.3 @@ -0,0 +1,50 @@
    10.4 +(* Title:  CalcElements/thmC.sml
    10.5 +   Author: Walther Neuper
    10.6 +   (c) due to copyright terms
    10.7 +
    10.8 +TODO: use "ThmC" for renaming identifiers.
    10.9 +Probably this structure can be dropped due to improvements of Isabelle.
   10.10 +*)
   10.11 +signature THEOREM_ISAC =
   10.12 +sig
   10.13 +(*datatype T = Rule_Def.Thm  ..ERROR: cannot get out from Rule_Def.rule*)
   10.14 +
   10.15 +  val string_of_thmI: thm -> string
   10.16 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   10.17 +  val thm2str: thm -> string
   10.18 +  val thms2str : thm list -> string
   10.19 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   10.20 +  val string_of_thm: thm -> string
   10.21 +  val string_of_thm': theory -> thm -> string
   10.22 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   10.23 +end
   10.24 +
   10.25 +(**)
   10.26 +structure ThmC(**): THEOREM_ISAC(**) =
   10.27 +struct
   10.28 +(**)
   10.29 +
   10.30 +(*datatype T = Rule_Def.Thm  ..ERROR: cannot get out from Rule_Def.rule*)
   10.31 + 
   10.32 +fun thm2str thm =
   10.33 +  let
   10.34 +    val t = Thm.prop_of thm
   10.35 +    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
   10.36 +    val ctxt' = Config.put show_markup false ctxt
   10.37 +  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
   10.38 +fun thms2str thms = (strs2str o (map thm2str)) thms
   10.39 +
   10.40 +(*check for [.] as caused by "fun assoc_thm'"*)
   10.41 +fun string_of_thm thm = Rule.term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
   10.42 +fun string_of_thm' thy thm = Rule.term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm)
   10.43 +fun string_of_thmI thm =
   10.44 +  let 
   10.45 +    val str = (de_quote o string_of_thm) thm
   10.46 +    val (a, b) = split_nlast (5, Symbol.explode str)
   10.47 +  in 
   10.48 +    case b of
   10.49 +      [" ", " ","[", ".", "]"] => implode a
   10.50 +    | _ => str
   10.51 +  end
   10.52 +
   10.53 +(**)end(**)

    11.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Wed Apr 08 16:56:47 2020 +0200
    11.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Thu Apr 09 11:21:53 2020 +0200
    11.3 @@ -2,19 +2,25 @@
    11.4     author: Walther Neuper
    11.5     0603
    11.6     (c) due to copyright terms
    11.7 +
    11.8 +TODO: use "Error_Fill_Pattern" for renaming identifiers -- go back to Rule_Def.*
    11.9  *)
   11.10  
   11.11 -signature ERROR_PATTERN =
   11.12 +signature ERROR_FILL_PATTERN =
   11.13  sig
   11.14 -  val find_fillpatterns : Calc.T -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
   11.15 +  type errpatID = Rule_Def.errpatID
   11.16 +  type errpat = errpatID * term list * thm list
   11.17 +  val errpats2str : errpat list -> string
   11.18 +
   11.19 +  val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID -> (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
   11.20    val is_exactly_equal : Calc.T -> string -> string * Tactic.input
   11.21    val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
   11.22      Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
   11.23    val mk_tacis: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
   11.24 -  val fetchErrorpatterns : Tactic.input -> Rule.errpatID list
   11.25 +  val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
   11.26    val check_for :
   11.27      term * term ->
   11.28 -    term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule_Set.T -> Rule.errpatID option
   11.29 +    term * (term * term) list -> (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T -> Error_Fill_Def.errpatID option
   11.30    val rule2thm'' : Rule.rule -> Celem.thm''
   11.31    val rule2rls' : Rule.rule -> string
   11.32  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   11.33 @@ -22,19 +28,21 @@
   11.34  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   11.35    val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
   11.36    val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
   11.37 -  val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule_Set.T -> Rule.errpatID option
   11.38 +  val check_err_patt : term * term -> Rule.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
   11.39    val get_fillform :
   11.40 -     'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option
   11.41 +     'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
   11.42    val get_fillpats :
   11.43 -     'a * (term * term) list -> term -> Rule.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list
   11.44 +     'a * (term * term) list -> term -> Error_Fill_Def.errpatID -> thm -> (Error_Fill_Def.fillpatID * term * thm * 'a) list
   11.45  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   11.46  
   11.47  end
   11.48  (**)
   11.49 -structure Error_Pattern(**): ERROR_PATTERN(**) =
   11.50 +structure Error_Fill_Pattern(**): ERROR_FILL_PATTERN(**) =
   11.51  struct
   11.52  (**)
   11.53  
   11.54 +type errpatID = Rule_Def.errpatID
   11.55 +
   11.56  fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
   11.57    | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule_Set.rule2str r);
   11.58  fun rule2rls' (Rule.Rls_ rls) = Rule_Set.id_rls rls
   11.59 @@ -162,8 +170,8 @@
   11.60      val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
   11.61      val subst = Rtools.get_bdv_subst prog env
   11.62      val errpatthms = errpats
   11.63 -      |> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID))
   11.64 -      |> map (#3: Rule.errpat -> thm list)
   11.65 +      |> filter ((curry op = errpatID) o (#1: Error_Fill_Def.errpat -> Error_Fill_Def.errpatID))
   11.66 +      |> map (#3: Error_Fill_Def.errpat -> thm list)
   11.67        |> flat
   11.68    in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
   11.69  
   11.70 @@ -211,6 +219,16 @@
   11.71    | Rule_Set.Empty => []
   11.72    end
   11.73  
   11.74 -(**)
   11.75 -end
   11.76 -(**)
   11.77 \ No newline at end of file
   11.78 +type errpatID = Rule_Def.errpatID
   11.79 +type errpat =
   11.80 +  errpatID    (* one identifier for a list of patterns                       
   11.81 +                 DESIGN ?TODO: errpatID list for hierarchy of errpats ?      *)
   11.82 +  * term list (* error patterns                                              *)
   11.83 +  * thm list  (* thms related to error patterns; note that respective lhs 
   11.84 +                 do not match (which reflects student's error).
   11.85 +                 fillpatterns are stored with these thms.                    *)
   11.86 +fun errpat2str (id, tms, thms) =
   11.87 +  "(\"" ^ id ^ "\",\n" ^ Rule.terms2str tms ^ ",\n" ^ ThmC.thms2str thms
   11.88 +fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
   11.89 +
   11.90 +(**)end(**)
   11.91 \ No newline at end of file

    12.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Apr 08 16:56:47 2020 +0200
    12.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Apr 09 11:21:53 2020 +0200
    12.3 @@ -622,12 +622,12 @@
    12.4      val fo = Calc.get_current_formula ptp
    12.5  	  val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
    12.6  	  val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
    12.7 -	  val (found, der) = Error_Pattern.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
    12.8 +	  val (found, der) = Error_Fill_Pattern.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
    12.9    in
   12.10      if found
   12.11      then
   12.12         let
   12.13 -         val tacis' = map (Error_Pattern.mk_tacis rew_ord erls) der;
   12.14 +         val tacis' = map (Error_Fill_Pattern.mk_tacis rew_ord erls) der;
   12.15  		     val (c', ptp) = Generate.embed_deriv tacis' ptp;
   12.16  	     in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
   12.17       else 

    13.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Wed Apr 08 16:56:47 2020 +0200
    13.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Apr 09 11:21:53 2020 +0200
    13.3 @@ -218,7 +218,7 @@
    13.4      val thm' = sym_thm thm
    13.5      val thmID' = case Symbol.explode thmID of
    13.6        "s" :: "y" :: "m" :: "_" :: id => implode id
    13.7 -    | "#" :: ":" :: _ => "#: " ^ Rule.string_of_thmI thm'
    13.8 +    | "#" :: ":" :: _ => "#: " ^ ThmC.string_of_thmI thm'
    13.9      | _ => "sym_" ^ thmID
   13.10    in Rule.Thm (thmID', thm') end
   13.11  | sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)

    14.1 --- a/src/Tools/isac/Interpret/step-solve.sml	Wed Apr 08 16:56:47 2020 +0200
    14.2 +++ b/src/Tools/isac/Interpret/step-solve.sml	Thu Apr 09 11:21:53 2020 +0200
    14.3 @@ -86,8 +86,8 @@
    14.4  (*
    14.5    Locate a step in a program, which has been determined by input of a term.
    14.6    Special case: if the term is a CAS-command, then create a calchead, and do 1 step.
    14.7 -  If "no derivation found" then Error_Pattern.check_for.
    14.8 -  (Error_Pattern.check_for *within* compare_step seems too expensive)
    14.9 +  If "no derivation found" then Error_Fill_Pattern.check_for.
   14.10 +  (Error_Fill_Pattern.check_for *within* compare_step seems too expensive)
   14.11  *)
   14.12  (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =*)
   14.13  fun by_term (pt, pos as (p, _)) istr =
   14.14 @@ -117,7 +117,7 @@
   14.15            		  | _ => error "inform: uncovered case of get_met"
   14.16            	  val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
   14.17            	in
   14.18 -          	  case Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of
   14.19 +          	  case Error_Fill_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of
   14.20            	    SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Chead.e_calcstate')
   14.21            	  | NONE => ("no derivation found", Chead.e_calcstate')
   14.22              end

    15.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Wed Apr 08 16:56:47 2020 +0200
    15.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Apr 09 11:21:53 2020 +0200
    15.3 @@ -135,7 +135,7 @@
    15.4      ("fill-inner-deriv",
    15.5        TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
    15.6      ("fill-all",
    15.7 -      TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Celem.fillpat list))
    15.8 +      TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Error_Fill_Def.fillpat list))
    15.9    ]
   15.10  \<close>
   15.11  

    16.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml	Wed Apr 08 16:56:47 2020 +0200
    16.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml	Thu Apr 09 11:21:53 2020 +0200
    16.3 @@ -209,7 +209,7 @@
    16.4  		   rls put_asm thm' ct;
    16.5  		 val _ = if pairopt <> NONE then () 
    16.6  			 else error("rewrite_set_, rewrite_ \""^
    16.7 -			 (string_of_thmI thm')^"\" \""^
    16.8 +			 (ThmC.string_of_thmI thm')^"\" \""^
    16.9  			 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
   16.10  	       in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
   16.11      val ruls = (#rules o Rule_Set.rep) ruless;
   16.12 @@ -245,7 +245,7 @@
   16.13  		   rls put_asm thm' ct;
   16.14  		 val _ = if pairopt <> NONE then () 
   16.15  			 else error("rewrite_set_, rewrite_ \""^
   16.16 -			 (string_of_thmI thm')^"\" \""^
   16.17 +			 (ThmC.string_of_thmI thm')^"\" \""^
   16.18  			 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
   16.19  	       in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
   16.20      val ruls = (#rules o Rule_Set.rep) ruless;

    17.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Wed Apr 08 16:56:47 2020 +0200
    17.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Thu Apr 09 11:21:53 2020 +0200
    17.3 @@ -158,7 +158,7 @@
    17.4                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
    17.5                      ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
    17.6                    val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ 
    17.7 -                    Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
    17.8 +                    ThmC.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
    17.9                    val _ = trace1 i (" calc. to: " ^ Rule.t2str thy ((fst o the) pairopt))
   17.10                  in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
   17.11              end
   17.12 @@ -172,7 +172,7 @@
   17.13                    val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
   17.14                      ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
   17.15                    val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
   17.16 -                     Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
   17.17 +                     ThmC.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
   17.18                    val _ = trace1 i (" cal1. to: " ^ Rule.t2str thy ((fst o the) pairopt))
   17.19                  in the pairopt end
   17.20              end
   17.21 @@ -299,7 +299,7 @@
   17.22  
   17.23  (* get the theorem associated with the xstring-identifier;
   17.24     if the identifier starts with "sym_" then swap lhs = rhs around =
   17.25 -   (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
   17.26 +   (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC.string_of_thmI);
   17.27     identifiers starting with "#" come from Num_Calc and
   17.28     get a hand-made theorem (containing numerals only) *)
   17.29  fun assoc_thm'' thy thmid =

    18.1 --- a/src/Tools/isac/Specify/appl.sml	Wed Apr 08 16:56:47 2020 +0200
    18.2 +++ b/src/Tools/isac/Specify/appl.sml	Thu Apr 09 11:21:53 2020 +0200
    18.3 @@ -377,7 +377,7 @@
    18.4          then
    18.5      	    case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of
    18.6      	      SOME (f', (id, thm))
    18.7 -    	        => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, Rule.string_of_thmI thm))))
    18.8 +    	        => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, ThmC.string_of_thmI thm))))
    18.9      	    | NONE => Notappl ("'calculate "^op_^"' not applicable") 
   18.10          else Notappl msg
   18.11        end

    19.1 --- a/src/Tools/isac/Specify/ptyps.sml	Wed Apr 08 16:56:47 2020 +0200
    19.2 +++ b/src/Tools/isac/Specify/ptyps.sml	Thu Apr 09 11:21:53 2020 +0200
    19.3 @@ -46,7 +46,7 @@
    19.4        Celem.pbt * Celem.pblID
    19.5    val prep_met : theory -> string -> string list -> Celem.pblID ->
    19.6       string list * (string * string list) list *
    19.7 -       {calc: 'a, crls: Rule_Set.T, errpats: Rule.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
    19.8 +       {calc: 'a, crls: Rule_Set.T, errpats: Error_Fill_Def.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
    19.9           rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
   19.10       Celem.met * Celem.metID
   19.11  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   19.12 @@ -55,7 +55,7 @@
   19.13    datatype match' = Matches' of Model.item Model.ppc | NoMatch' of Model.item Model.ppc
   19.14    val match_pbl : Selem.fmz_ -> Celem.pbt -> match'
   19.15    val refine : Selem.fmz_ -> Celem.pblID -> Stool.match list
   19.16 -  val e_errpat : Rule.errpat
   19.17 +  val e_errpat : Error_Fill_Def.errpat
   19.18    val show_pblguhs : unit -> unit
   19.19    val sort_pblguhs : unit -> unit
   19.20  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   19.21 @@ -275,7 +275,7 @@
   19.22          |> map flattup;
   19.23      in (oris, ctxt) end;
   19.24  
   19.25 -val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Rule.errpat
   19.26 +val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Error_Fill_Def.errpat
   19.27  val e_fillpat = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
   19.28  
   19.29  (** breadth-first search on hierarchy of problem-types **)

    20.1 --- a/src/Tools/isac/TODO.thy	Wed Apr 08 16:56:47 2020 +0200
    20.2 +++ b/src/Tools/isac/TODO.thy	Thu Apr 09 11:21:53 2020 +0200
    20.3 @@ -39,7 +39,7 @@
    20.4    \item see "TODO CLEANUP Thm" in code
    20.5      (* TODO CLEANUP Thm:
    20.6      Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
    20.7 -                       (b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI
    20.8 +                       (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC.string_of_thmI
    20.9      thmID            : type for data from user input + program
   20.10      thmDeriv         : type for thy_hierarchy ONLY
   20.11      obsolete types   : thm' (SEE "ad thm'"), thm''. 

    21.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Apr 08 16:56:47 2020 +0200
    21.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Apr 09 11:21:53 2020 +0200
    21.3 @@ -97,7 +97,8 @@
    21.4    open Env;
    21.5    open LI;                     scan_dn;
    21.6    open Istate;
    21.7 -  open Error_Pattern;
    21.8 +  open Error_Fill_Pattern;
    21.9 +  open Error_Fill_Def;
   21.10    open In_Chead;
   21.11    open Rtools;                 trtas2str;
   21.12    open Chead;                  pt_extract;
   21.13 @@ -126,7 +127,12 @@
   21.14    open Num_Calc;                   get_pair;
   21.15    open TermC;                  atomt;
   21.16    open Celem;                  e_pbt;
   21.17 -  open Rule;                   string_of_thm;
   21.18 +  open Rule;
   21.19 +  open Rule_Set
   21.20 +  open Exec_Def
   21.21 +  open ThyC
   21.22 +  open ThmC
   21.23 +  open Rewrite_Ord
   21.24  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   21.25  \<close>
   21.26  
   21.27 @@ -142,6 +148,14 @@
   21.28  ML \<open>
   21.29  \<close> ML \<open>
   21.30  \<close> ML \<open>
   21.31 +\<close> ML \<open>
   21.32 +\<close> ML \<open>
   21.33 +\<close> ML \<open>
   21.34 +\<close> ML \<open>
   21.35 +\<close> ML \<open>
   21.36 +\<close> ML \<open>
   21.37 +\<close> ML \<open>
   21.38 +\<close> ML \<open>
   21.39  \<close>
   21.40  
   21.41  ML \<open>

    22.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Wed Apr 08 16:56:47 2020 +0200
    22.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Thu Apr 09 11:21:53 2020 +0200
    22.3 @@ -97,7 +97,8 @@
    22.4    open Env;
    22.5    open LI;                     scan_dn;
    22.6    open Istate;
    22.7 -  open Error_Pattern;
    22.8 +  open Error_Fill_Pattern;
    22.9 +  open Error_Fill_Def;
   22.10    open In_Chead;
   22.11    open Rtools;                 trtas2str;
   22.12    open Chead;                  pt_extract;
   22.13 @@ -126,10 +127,11 @@
   22.14    open Num_Calc;                   get_pair;
   22.15    open TermC;                  atomt;
   22.16    open Celem;                  e_pbt;
   22.17 -  open Rule;                   string_of_thm;
   22.18 +  open Rule;
   22.19    open Rule_Set
   22.20    open Exec_Def
   22.21    open ThyC
   22.22 +  open ThmC
   22.23    open Rewrite_Ord
   22.24  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   22.25  \<close>

    23.1 --- a/test/Tools/isac/Test_Some.thy	Wed Apr 08 16:56:47 2020 +0200
    23.2 +++ b/test/Tools/isac/Test_Some.thy	Thu Apr 09 11:21:53 2020 +0200
    23.3 @@ -12,11 +12,14 @@
    23.4    open Test_Code;              CalcTreeTEST;
    23.5    open LItool;                 arguments_from_model;
    23.6    open Sub_Problem;
    23.7 +  open Fetch_Tacs;
    23.8    open Step
    23.9    open Env;
   23.10    open LI;                     scan_dn;
   23.11    open Istate;
   23.12 -  open Error_Pattern;
   23.13 +  open Error_Fill_Pattern;
   23.14 +  open Error_Fill_Def;
   23.15 +  open In_Chead;
   23.16    open Rtools;                 trtas2str;
   23.17    open Chead;                  pt_extract;
   23.18    open Generate;               (* NONE *)
   23.19 @@ -44,7 +47,12 @@
   23.20    open Num_Calc;                   get_pair;
   23.21    open TermC;                  atomt;
   23.22    open Celem;                  e_pbt;
   23.23 -  open Rule;                   string_of_thm;
   23.24 +  open Rule;
   23.25 +  open Rule_Set
   23.26 +  open Exec_Def
   23.27 +  open ThyC
   23.28 +  open ThmC
   23.29 +  open Rewrite_Ord
   23.30  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
   23.31  \<close>
   23.32  ML_file "CalcElements/libraryC.sml"