1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4      then 
     1.5        let 
     1.6          val thy' = Ctree.get_obj Ctree.g_domID pt p'
     1.7 -        val {rew_ord', erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt p')              
     1.8 +        val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p')              
     1.9  	    in ("OK", thy', rew_ord', erls, false) end
    1.10       else 
    1.11        let
    1.12 @@ -69,7 +69,7 @@
    1.13      then
    1.14        let
    1.15          val thy' = Ctree.get_obj Ctree.g_domID pt p'
    1.16 -        val {calc = scr_isa_fns, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt p')
    1.17 +        val {calc = scr_isa_fns, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt p')
    1.18          val opt = assoc (scr_isa_fns, scrop)
    1.19  	    in
    1.20  	      case opt of
    1.21 @@ -154,7 +154,7 @@
    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 {rew_ord' = ro', erls = erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt pp);
    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        in 
    1.30 @@ -188,14 +188,14 @@
    1.31          | NONE => Applicable.No (rls ^ " not applicable")
    1.32        end
    1.33    | check (Tactic.Subproblem (domID, pblID)) (_, _) = 
    1.34 -      Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [], 
    1.35 +      Applicable.Yes (Tactic.Subproblem' ((domID, pblID, MethodC.id_empty), [], 
    1.36  			  TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
    1.37    | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
    1.38        let
    1.39          val pp = Ctree.par_pblobj pt p
    1.40          val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
    1.41          val f = Calc.current_formula cs;
    1.42 -		    val {rew_ord', erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt pp)
    1.43 +		    val {rew_ord', erls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp)
    1.44  		    val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
    1.45  		    val subst = Subst.T_from_string_eqs thy sube
    1.46  		    val ro = Rewrite_Ord.assoc_rew_ord rew_ord'