1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Tue May 12 17:42:29 2020 +0200
     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, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')              
     1.8 +        val {rew_ord', erls, ...} = Method.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, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
    1.17 +        val {calc = scr_isa_fns, ...} = Method.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 @@ -98,7 +98,7 @@
    1.22          val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
    1.23            Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
    1.24          | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
    1.25 -        val {where_, ...} = Specify.get_pbt pI
    1.26 +        val {where_, ...} = Problem.from_store pI
    1.27          val pres = map (I_Model.mk_env probl |> subst_atomic) where_
    1.28          val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
    1.29            then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
    1.30 @@ -154,7 +154,7 @@
    1.31          val pp = Ctree.par_pblobj pt p;
    1.32          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.33          val thy = ThyC.get_theory thy';
    1.34 -        val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
    1.35 +        val {rew_ord' = ro', erls = erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt pp);
    1.36          val f = Calc.current_formula cs;
    1.37          val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
    1.38        in 
    1.39 @@ -195,7 +195,7 @@
    1.40          val pp = Ctree.par_pblobj pt p
    1.41          val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
    1.42          val f = Calc.current_formula cs;
    1.43 -		    val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
    1.44 +		    val {rew_ord', erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt pp)
    1.45  		    val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
    1.46  		    val subst = Subst.T_from_string_eqs thy sube
    1.47  		    val ro = Rewrite_Ord.assoc_rew_ord rew_ord'