1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Fri Oct 07 20:46:48 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Sat Oct 08 11:40:48 2022 +0200
     1.3 @@ -43,13 +43,13 @@
     1.4  
     1.5  fun get_ruleset _ (pos as (p, _)) pt = 
     1.6    let 
     1.7 -    val (pbl, p', rls', ctxt) = LItool.parent_node_PIDE pt pos
     1.8 +    val (pbl, p', rls', ctxt) = LItool.parent_node pt pos
     1.9    in                                                      
    1.10      if pbl
    1.11      then 
    1.12        let 
    1.13          val thy' = Ctree.get_obj Ctree.g_domID pt p'
    1.14 -        val {rew_ord', erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt p')              
    1.15 +        val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt p')              
    1.16  	    in ("OK", thy', rew_ord', erls, false) end
    1.17       else 
    1.18        let
    1.19 @@ -60,13 +60,13 @@
    1.20  
    1.21  fun get_eval scrop (pos as (p, _)) pt = 
    1.22    let
    1.23 -    val (pbl, p', rls', ctxt) =  LItool.parent_node_PIDE pt pos
    1.24 +    val (pbl, p', rls', ctxt) =  LItool.parent_node pt pos
    1.25    in
    1.26      if pbl
    1.27      then
    1.28        let
    1.29          val thy' = Ctree.get_obj Ctree.g_domID pt p'
    1.30 -        val {calc = scr_isa_fns, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt p')
    1.31 +        val {calc = scr_isa_fns, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt p')
    1.32          val opt = assoc (scr_isa_fns, scrop)
    1.33  	    in
    1.34  	      case opt of
    1.35 @@ -95,7 +95,7 @@
    1.36          val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
    1.37            Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
    1.38          | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
    1.39 -        val {where_, ...} = Problem.from_store_PIDE ctxt pI
    1.40 +        val {where_, ...} = Problem.from_store ctxt pI
    1.41          val pres = map (I_Model.environment probl |> subst_atomic) where_
    1.42          val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
    1.43            then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
    1.44 @@ -152,7 +152,7 @@
    1.45          val pp = Ctree.par_pblobj pt p;
    1.46          val ctxt = Ctree.get_loc pt pos |> snd
    1.47          val thy = Proof_Context.theory_of ctxt
    1.48 -        val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp);
    1.49 +        val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp);
    1.50          val f = Calc.current_formula cs;
    1.51          val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
    1.52        in 
    1.53 @@ -195,7 +195,7 @@
    1.54          val ctxt = Ctree.get_loc pt pos |> snd
    1.55          val thy = Proof_Context.theory_of ctxt
    1.56          val f = Calc.current_formula cs;
    1.57 -		    val {rew_ord', erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp)
    1.58 +		    val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
    1.59  		    val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*)
    1.60  		    val ro = get_rew_ord ctxt rew_ord'
    1.61  		  in