1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Sat Aug 06 19:05:33 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Tue Aug 16 12:21:21 2022 +0200
     1.3 @@ -147,12 +147,18 @@
     1.4            | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") 
     1.5          else Applicable.No msg
     1.6        end
     1.7 -  | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) = 
     1.8 +  | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, pos as (p, _))) = 
     1.9        let 
    1.10          val pp = Ctree.par_pblobj pt p;
    1.11 +(*ctxt*)
    1.12          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.13          val thy = ThyC.get_theory thy';
    1.14          val ctxt = Proof_Context.init_global thy;
    1.15 +(*ctxt* )
    1.16 +val ctxt = Ctree.get_loc pt pos |> snd
    1.17 +val thy = Proof_Context.theory_of ctxt
    1.18 +val thy' = Context.theory_name thy
    1.19 +( *ctxt*)
    1.20          val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp);
    1.21          val f = Calc.current_formula cs;
    1.22          val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
    1.23 @@ -162,10 +168,16 @@
    1.24              Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
    1.25          | NONE => Applicable.No (fst thm ^ " not applicable")
    1.26        end
    1.27 -  | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
    1.28 +  | check (Tactic.Rewrite_Set rls) (cs as (pt, pos as (p, _))) =
    1.29        let 
    1.30 +(*ctxt*)
    1.31          val pp = Ctree.par_pblobj pt p; 
    1.32          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.33 +(*ctxt* )
    1.34 +val ctxt = Ctree.get_loc pt pos |> snd
    1.35 +val thy = Proof_Context.theory_of ctxt
    1.36 +val thy' = Context.theory_name thy
    1.37 +( *ctxt*)
    1.38          val f = Calc.current_formula cs;
    1.39        in
    1.40          case Rewrite.rewrite_set_ (ThyC.id_to_ctxt thy') false (assoc_rls rls) f of
    1.41 @@ -173,12 +185,18 @@
    1.42              => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
    1.43            | NONE => Applicable.No (rls ^ " not applicable")
    1.44        end
    1.45 -  | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) =
    1.46 +  | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, pos as (p, _))) =
    1.47        let 
    1.48 +(*ctxt*)
    1.49          val pp = Ctree.par_pblobj pt p;
    1.50          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.51          val thy = ThyC.get_theory thy';
    1.52          val ctxt = Proof_Context.init_global thy;
    1.53 +(*ctxt* )
    1.54 +val ctxt = Ctree.get_loc pt pos |> snd
    1.55 +val thy = Proof_Context.theory_of ctxt
    1.56 +val thy' = Context.theory_name thy
    1.57 +( *ctxt*)
    1.58          val f = Calc.current_formula cs;
    1.59      	  val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
    1.60        in 
    1.61 @@ -190,11 +208,17 @@
    1.62    | check (Tactic.Subproblem (domID, pblID)) (_, _) = 
    1.63        Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [], 
    1.64  			  TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
    1.65 -  | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
    1.66 +  | check (Tactic.Substitute sube) (cs as (pt, pos as (p, _))) =
    1.67        let
    1.68          val pp = Ctree.par_pblobj pt p
    1.69 +(*ctxt*)
    1.70          val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
    1.71          val ctxt = Proof_Context.init_global thy;
    1.72 +(*ctxt* )
    1.73 +val ctxt = Ctree.get_loc pt pos |> snd
    1.74 +val thy = Proof_Context.theory_of ctxt
    1.75 +val thy' = Context.theory_name thy
    1.76 +( *ctxt*)
    1.77          val f = Calc.current_formula cs;
    1.78  		    val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
    1.79  		    val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
    1.80 @@ -215,9 +239,15 @@
    1.81  		  end
    1.82    | check (Tactic.Tac id) (cs as (pt, (p, _))) =
    1.83        let 
    1.84 +(*ctxt*)
    1.85          val pp = Ctree.par_pblobj pt p; 
    1.86          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.87          val thy = ThyC.get_theory thy';
    1.88 +(*ctxt* )
    1.89 +val ctxt = Ctree.get_loc pt pos |> snd
    1.90 +val thy = Proof_Context.theory_of ctxt
    1.91 +val thy' = Context.theory_name thy
    1.92 +( *ctxt*)
    1.93          val f = Calc.current_formula cs;
    1.94        in
    1.95          Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))