1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4        in
     1.5          if msg = "OK"
     1.6          then
     1.7 -    	    case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
     1.8 +    	    case Rewrite.calculate_ (ThyC.id_to_ctxt thy') isa_fn f of
     1.9      	      SOME (f', (id, thm))
    1.10      	        => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
    1.11      	    | NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable") 
    1.12 @@ -136,7 +136,7 @@
    1.13    | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) = 
    1.14        let
    1.15          val (msg, thy', ro, rls', _) = get_ruleset thm p pt;
    1.16 -        val thy = ThyC.get_theory thy';
    1.17 +        val thy = ThyC.id_to_ctxt thy';
    1.18          val f = Calc.current_formula cs;
    1.19        in
    1.20          if msg = "OK" 
    1.21 @@ -151,11 +151,12 @@
    1.22          val pp = Ctree.par_pblobj pt p;
    1.23          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.24          val thy = ThyC.get_theory thy';
    1.25 +        val ctxt = Proof_Context.init_global thy;
    1.26          val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp);
    1.27          val f = Calc.current_formula cs;
    1.28 -        val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
    1.29 +        val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
    1.30        in 
    1.31 -        case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
    1.32 +        case Rewrite.rewrite_inst_ ctxt (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
    1.33            SOME (f', asm) =>
    1.34              Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
    1.35          | NONE => Applicable.No (fst thm ^ " not applicable")
    1.36 @@ -166,7 +167,7 @@
    1.37          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.38          val f = Calc.current_formula cs;
    1.39        in
    1.40 -        case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
    1.41 +        case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of
    1.42            SOME (f', asm)
    1.43              => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
    1.44            | NONE => Applicable.No (rls ^ " not applicable")
    1.45 @@ -176,10 +177,11 @@
    1.46          val pp = Ctree.par_pblobj pt p;
    1.47          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.48          val thy = ThyC.get_theory thy';
    1.49 +        val ctxt = Proof_Context.init_global thy;
    1.50          val f = Calc.current_formula cs;
    1.51 -    	  val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
    1.52 +    	  val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
    1.53        in 
    1.54 -        case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
    1.55 +        case Rewrite.rewrite_set_inst_ ctxt false subst (assoc_rls rls) f of
    1.56            SOME (f', asm)
    1.57              => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
    1.58          | NONE => Applicable.No (rls ^ " not applicable")
    1.59 @@ -191,6 +193,7 @@
    1.60        let
    1.61          val pp = Ctree.par_pblobj pt p
    1.62          val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
    1.63 +        val ctxt = Proof_Context.init_global thy;
    1.64          val f = Calc.current_formula cs;
    1.65  		    val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
    1.66  		    val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
    1.67 @@ -205,7 +208,7 @@
    1.68  		        else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
    1.69  		      end
    1.70  		    else (*2*)
    1.71 -		      case Rewrite.rewrite_terms_ thy ro erls subte f of
    1.72 +		      case Rewrite.rewrite_terms_ ctxt ro erls subte f of
    1.73  		        SOME (f', _) =>  Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
    1.74  		      | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
    1.75  		  end