1.1 --- a/TODO.md	Sat Aug 06 18:00:33 2022 +0200
     1.2 +++ b/TODO.md	Sat Aug 06 18:50:43 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 -    - Derive.steps
     1.8      - Fetch_Tacs.specific_from_prog ?
     1.9      - Eval.adhoc_thm, adhoc_thm1_
    1.10      - ? LIST IS NOT COMPLETE
    1.11 @@ -67,6 +66,7 @@
    1.12          val thy = ThyC.get_theory thy';              ->   val thy = Proof_Context.theory_of ctxt
    1.13          val ctxt = Proof_Context.init_global thy;    ->   val thy' = Context.theory_name thy
    1.14        cp code to test/*
    1.15 +    - Derive.steps: note HACK
    1.16  
    1.17  * WN: eliminate SPARK; as an example replaced by Outer_Syntax.command..problem
    1.18  

     2.1 --- a/src/Tools/isac/Interpret/derive.sml	Sat Aug 06 18:00:33 2022 +0200
     2.2 +++ b/src/Tools/isac/Interpret/derive.sml	Sat Aug 06 18:50:43 2022 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4      term option -> term -> derivation
     2.5    val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
     2.6      term option -> term -> rule_result list
     2.7 -  val steps : Rewrite_Ord.T -> Rule_Set.T -> Rule.rule list -> term -> term ->
     2.8 +  val steps : Proof.context -> Rewrite_Ord.T -> Rule_Set.T -> Rule.rule list -> term -> term ->
     2.9      bool * derivation
    2.10    val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
    2.11  \<^isac_test>\<open>
    2.12 @@ -116,13 +116,13 @@
    2.13  fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
    2.14  
    2.15  (* fo = ifo excluded already in inform *)
    2.16 -fun steps rew_ord erls rules fo ifo =
    2.17 +fun steps ctxt rew_ord erls rules fo ifo =
    2.18    let 
    2.19      fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
    2.20        | derivat dt = (#1 o #3 o last_elem) dt
    2.21      fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
    2.22 -    val  fod = do_one (Proof_Context.init_global (ThyC.Isac())) erls rules (snd rew_ord) NONE  fo
    2.23 -    val ifod = do_one (Proof_Context.init_global (ThyC.Isac())) erls rules (snd rew_ord) NONE ifo
    2.24 +    val  fod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(**) erls rules (snd rew_ord) NONE  fo
    2.25 +    val ifod = do_one (** )ctxt( *HACK*)(Proof_Context.init_global (ThyC.Isac()))(**) erls rules (snd rew_ord) NONE ifo
    2.26    in 
    2.27      case (fod, ifod) of
    2.28        ([], []) => if fo = ifo then (true, []) else (false, [])

     3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Aug 06 18:00:33 2022 +0200
     3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Aug 06 18:50:43 2022 +0200
     3.3 @@ -617,7 +617,7 @@
     3.4      val fo = Calc.current_formula ptp
     3.5  	  val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
     3.6  	  val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
     3.7 -	  val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
     3.8 +	  val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)
     3.9    in
    3.10      if found
    3.11      then

     4.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml	Sat Aug 06 18:00:33 2022 +0200
     4.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml	Sat Aug 06 18:50:43 2022 +0200
     4.3 @@ -317,7 +317,7 @@
     4.4  			| _ => TermC.empty (*on PblObj is fo <> ifo*);
     4.5  	  val {nrls, ...} = MethodC.from_store (get_obj g_metID pt (par_pblobj pt p))
     4.6  	  val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
     4.7 -	  (*val (found, der) = *)Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
     4.8 +	  (*val (found, der) = *)Derive.steps ctxt rew_ord erls rules fo ifo; (*<---------------*)
     4.9  "~~~~~ fun .concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
    4.10    (rew_ord, erls, rules, fo, ifo);
    4.11      fun derivat ([]:(term * rule * (term * term list)) list) = TermC.empty

     5.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Sat Aug 06 18:00:33 2022 +0200
     5.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Sat Aug 06 18:50:43 2022 +0200
     5.3 @@ -113,7 +113,7 @@
     5.4      val fo = Calc.current_formula ptp
     5.5  	  val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
     5.6  	  val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
     5.7 -	  val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
     5.8 +	  val (found, der) = Derive.steps ctxt rew_ord erls rules fo ifo; (*<---------------*)
     5.9      (*if*) found (*then*);
    5.10           val tacis' = map (State_Steps.make_single rew_ord erls) der;
    5.11