1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Fri Sep 09 10:15:28 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Fri Sep 09 10:53:51 2022 +0200
     1.3 @@ -251,11 +251,13 @@
     1.4  ML \<open>
     1.5  val get_ref_thy = KEStore_Elems.get_ref_thy;
     1.6  
     1.7 +(*
     1.8  fun assoc' ([], key) = raise ERROR ("ME_Isa: rew_ord \"" ^ key ^ "\" not in system 2")
     1.9    | assoc' ((keyi, xi) :: pairs, key) =
    1.10      if key = keyi then SOME xi else assoc' (pairs, key);
    1.11  fun assoc_rew_ord thy ro = ((the o assoc') (KEStore_Elems.get_rew_ords thy, ro))
    1.12    handle ERROR _ => raise ERROR ("ME_Isa: rew_ord \"" ^ ro ^ "\" not in system 1");
    1.13 +*)
    1.14  fun get_rew_ord ctxt (id: Rewrite_Ord.id) = 
    1.15    case AList.lookup (op =) (KEStore_Elems.get_rew_ords (Proof_Context.theory_of ctxt)) id of
    1.16      SOME function => function: Rewrite_Ord.function

     2.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Fri Sep 09 10:15:28 2022 +0200
     2.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Fri Sep 09 10:53:51 2022 +0200
     2.3 @@ -142,7 +142,7 @@
     2.4        in
     2.5          if msg = "OK" 
     2.6          then
     2.7 -          case Rewrite.rewrite_ ctxt (assoc_rew_ord thy ro) rls' false (snd thm) f of
     2.8 +          case Rewrite.rewrite_ ctxt (get_rew_ord ctxt ro) rls' false (snd thm) f of
     2.9              SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
    2.10            | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") 
    2.11          else Applicable.No msg
    2.12 @@ -156,7 +156,7 @@
    2.13          val f = Calc.current_formula cs;
    2.14          val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
    2.15        in 
    2.16 -        case Rewrite.rewrite_inst_ ctxt (assoc_rew_ord thy ro') erls false subst (snd thm) f of
    2.17 +        case Rewrite.rewrite_inst_ ctxt (get_rew_ord ctxt ro') erls false subst (snd thm) f of
    2.18            SOME (f', asm) =>
    2.19              Applicable.Yes (Tactic.Rewrite_Inst' 
    2.20                (Context.theory_name thy, ro', erls, false, subst, thm, f, (f', asm)))
    2.21 @@ -197,7 +197,7 @@
    2.22          val f = Calc.current_formula cs;
    2.23  		    val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
    2.24  		    val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*)
    2.25 -		    val ro = assoc_rew_ord thy rew_ord'
    2.26 +		    val ro = get_rew_ord ctxt rew_ord'
    2.27  		  in
    2.28  		    if foldl and_ (true, map TermC.contains_Var subte)
    2.29  		    then (*1*)

     3.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Fri Sep 09 10:15:28 2022 +0200
     3.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Fri Sep 09 10:53:51 2022 +0200
     3.3 @@ -271,9 +271,9 @@
     3.4      try_rew ctxt Rewrite_Ord.empty Rule_Set.empty [] f 
     3.5        (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))
     3.6    | applicable ctxt ro erls f (Rewrite thm'') =
     3.7 -    try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'')
     3.8 +    try_rew ctxt (ro, get_rew_ord ctxt ro) erls [] f (Rule.Thm thm'')
     3.9    | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) =
    3.10 -    try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls 
    3.11 +    try_rew ctxt (ro, get_rew_ord ctxt ro) erls 
    3.12        (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
    3.13  
    3.14    | applicable ctxt _ _ f (Rewrite_Set rls') =