1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 03 13:22:36 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Wed Aug 03 17:18:47 2022 +0200
     1.3 @@ -136,12 +136,13 @@
     1.4    | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) = 
     1.5        let
     1.6          val (msg, thy', ro, rls', _) = get_ruleset thm p pt;
     1.7 -        val thy = ThyC.id_to_ctxt thy';
     1.8 +        val thy = ThyC.get_theory thy';
     1.9 +        val ctxt = Proof_Context.init_global thy;
    1.10          val f = Calc.current_formula cs;
    1.11        in
    1.12          if msg = "OK" 
    1.13          then
    1.14 -          case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of
    1.15 +          case Rewrite.rewrite_ ctxt (assoc_rew_ord thy ro) rls' false (snd thm) f of
    1.16              SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
    1.17            | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") 
    1.18          else Applicable.No msg
    1.19 @@ -156,7 +157,7 @@
    1.20          val f = Calc.current_formula cs;
    1.21          val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
    1.22        in 
    1.23 -        case Rewrite.rewrite_inst_ ctxt (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
    1.24 +        case Rewrite.rewrite_inst_ ctxt (assoc_rew_ord thy ro') erls false subst (snd thm) f of
    1.25            SOME (f', asm) =>
    1.26              Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
    1.27          | NONE => Applicable.No (fst thm ^ " not applicable")
    1.28 @@ -198,7 +199,7 @@
    1.29  		    val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
    1.30  		    val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
    1.31  		    val subst = Subst.T_from_string_eqs thy sube
    1.32 -		    val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
    1.33 +		    val ro = assoc_rew_ord thy rew_ord'
    1.34  		  in
    1.35  		    if foldl and_ (true, map TermC.contains_Var subte)
    1.36  		    then (*1*)