1.1 --- a/TODO.md	Sat Aug 06 17:36:59 2022 +0200
     1.2 +++ b/TODO.md	Sat Aug 06 18:00:33 2022 +0200
     1.3 @@ -55,7 +55,6 @@
     1.4  ***** priority of WN items is top down, most urgent/simple on top
     1.5  
     1.6  * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
     1.7 -    - Error_Pattern.fill_form
     1.8      - Derive.steps
     1.9      - Fetch_Tacs.specific_from_prog ?
    1.10      - Eval.adhoc_thm, adhoc_thm1_

     2.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 17:36:59 2022 +0200
     2.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 18:00:33 2022 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4  
     2.5    type record
     2.6  
     2.7 -  val from_store: Tactic.input -> Error_Pattern_Def.id list
     2.8 +  val from_store:  Tactic.input -> Error_Pattern_Def.id list
     2.9    val filled_exactly: Calc.T -> string -> string * Tactic.input
    2.10    val check_for: Proof.context -> term * term -> term * Env.T -> T list * Rule_Set.T -> id option
    2.11  
    2.12 @@ -28,9 +28,9 @@
    2.13  
    2.14  \<^isac_test>\<open>
    2.15    val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id option
    2.16 -  val fill_from_store: Subst.input option * Subst.T -> term -> id -> thm ->
    2.17 +  val fill_from_store: Proof.context -> Subst.input option * Subst.T -> term -> id -> thm ->
    2.18      record list
    2.19 -  val fill_form: Subst.input option * Subst.T -> thm * term -> id -> fill_in ->
    2.20 +  val fill_form: Proof.context -> Subst.input option * Subst.T -> thm * term -> id -> fill_in ->
    2.21      record option
    2.22  \<close>
    2.23  end
    2.24 @@ -95,9 +95,8 @@
    2.25  
    2.26  (* fill-in patterns an forms.
    2.27    returns thm required by "fun in_fillform *)
    2.28 -fun fill_form (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =
    2.29 +fun fill_form ctxt (subs_opt, subst) (thm, form) id (fillpatID, pat, erpaID) =
    2.30    let
    2.31 -    val ctxt = Proof_Context.init_global ((ThyC.Isac()))
    2.32      val (form', _, _, rewritten) =
    2.33        Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
    2.34    in (*the fillpat of the thm must be dedicated to id*)
    2.35 @@ -106,7 +105,7 @@
    2.36      else NONE
    2.37    end
    2.38  
    2.39 -fun fill_from_store subst form id thm =
    2.40 +fun fill_from_store ctxt subst form id thm =
    2.41    let
    2.42      val thmDeriv = Thm.get_name_hint thm
    2.43      val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
    2.44 @@ -114,7 +113,7 @@
    2.45      val fillpats = case Thy_Read.from_store theID of
    2.46        Thy_Write.Hthm {fillpats, ...} => fillpats
    2.47      | _ => raise ERROR "fill_from_store: uncovered case of get_the"
    2.48 -    val some = map (fill_form subst (thm, form) id) fillpats
    2.49 +    val some = map (fill_form ctxt subst (thm, form) id) fillpats
    2.50    in some |> filter is_some |> map the end
    2.51  
    2.52  fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =
    2.53 @@ -130,7 +129,7 @@
    2.54        |> filter ((curry op = id) o (#1: Error_Pattern_Def.T -> Error_Pattern_Def.id))
    2.55        |> map (#3: Error_Pattern_Def.T -> thm list)
    2.56        |> flat
    2.57 -  in map (fill_from_store subst f_curr id) errpatthms |> flat end
    2.58 +  in map (fill_from_store (Ctree.get_ctxt pt pos) subst f_curr id) errpatthms |> flat end
    2.59  
    2.60  (*
    2.61    Check input on a fill-pattern:

     3.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 17:36:59 2022 +0200
     3.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sat Aug 06 18:00:33 2022 +0200
     3.3 @@ -329,7 +329,7 @@
     3.4  "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
     3.5  "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
     3.6  "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
     3.7 - reset_states ();
     3.8 + reset_states (); 
     3.9   CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], 
    3.10  	    ("Test", ["sqroot-test", "univariate", "equation", "test"],
    3.11  	     ["Test", "squ-equ-test-subpbl1"]))];
    3.12 @@ -1095,7 +1095,7 @@
    3.13        |> map (#3: Error_Pattern.T -> thm list)
    3.14        |> flat;
    3.15  
    3.16 -case map (Error_Pattern.fill_from_store subst f_curr errpatID) errpatthms |> flat of
    3.17 +case map (Error_Pattern.fill_from_store ctxt subst f_curr errpatID) errpatthms |> flat of
    3.18    ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if UnparseC.term tm = 
    3.19      "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
    3.20      then () else error "find_fill_patterns changed 1a"
    3.21 @@ -1107,7 +1107,7 @@
    3.22          val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
    3.23          val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
    3.24          val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store theID
    3.25 -        val some = map (Error_Pattern.fill_form subst (thm, form) errpatID) fillpats;
    3.26 +        val some = map (Error_Pattern.fill_form ctxt subst (thm, form) errpatID) fillpats;
    3.27  
    3.28  case some |> filter is_some |> map the of
    3.29    ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm = 
    3.30 @@ -1125,7 +1125,7 @@
    3.31  else error "find_fill_patterns changed 3";
    3.32  
    3.33  "~~~~~ to findFillpatterns return val:"; val (fillpats) =
    3.34 -  (map (Error_Pattern.fill_from_store (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
    3.35 +  (map (Error_Pattern.fill_from_store ctxt (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
    3.36  
    3.37  "vvv--- dropped this code WN120730";
    3.38  val msg = "fill patterns " ^