1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Fri Oct 07 20:46:48 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Sat Oct 08 11:40:48 2022 +0200
     1.3 @@ -13,10 +13,10 @@
     1.4    | Not_Associated;
     1.5    val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
     1.6    
     1.7 -  val parent_node_PIDE: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T * Proof.context
     1.8 +  val parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T * Proof.context
     1.9    val init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> MethodC.id ->
    1.10      Istate.T * Proof.context * Program.T
    1.11 -  val resume_prog_PIDE: Pos.pos' -> Ctree.ctree -> 
    1.12 +  val resume_prog: Pos.pos' -> Ctree.ctree -> 
    1.13      (Istate.T * Proof.context) * Program.T
    1.14  
    1.15    val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term -> 
    1.16 @@ -61,7 +61,7 @@
    1.17        case find_first (test_dsc d) itms of
    1.18          NONE => raise ERROR (error_msg_2 d itms)
    1.19        | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
    1.20 -    val pats = (#ppc o MethodC.from_store_PIDE ctxt) mI
    1.21 +    val pats = (#ppc o MethodC.from_store ctxt) mI
    1.22      val _ = if pats = [] then raise ERROR error_msg_1 else ()
    1.23    in (flat o (map (itm2arg itms))) pats end;
    1.24  
    1.25 @@ -204,8 +204,8 @@
    1.26      (trace_msg_3 ctxt tac; Not_Associated);
    1.27  
    1.28  (* find the next parent, which is either a PblObj xor a PrfObj in case of detail step*)
    1.29 -fun parent_node_PIDE _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
    1.30 -  | parent_node_PIDE pt (pos as (p, _)) =
    1.31 +fun parent_node _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
    1.32 +  | parent_node pt (pos as (p, _)) =
    1.33      let
    1.34        fun par _ [] = (true, [], Rule_Set.Empty, ContextC.empty)
    1.35          | par pt p =
    1.36 @@ -273,7 +273,7 @@
    1.37    let
    1.38      val actuals = arguments_from_model ctxt metID itms
    1.39      val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
    1.40 -    val (scr, sc) = (case (#scr o MethodC.from_store_PIDE ctxt) metID of
    1.41 +    val (scr, sc) = (case (#scr o MethodC.from_store ctxt) metID of
    1.42             scr as Rule.Prog sc => (trace_init ctxt metID; (scr, sc))
    1.43         | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string metID))
    1.44      val formals = Program.formal_args sc    
    1.45 @@ -290,7 +290,7 @@
    1.46          else
    1.47            let val (f, a) = assoc_by_type f aas
    1.48            in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
    1.49 -    val {pre, prls, ...} = MethodC.from_store_PIDE ctxt metID;
    1.50 +    val {pre, prls, ...} = MethodC.from_store ctxt metID;
    1.51      val pres = Pre_Conds.check prls pre itms 0 |> snd |> map snd;
    1.52      val ctxt = ctxt |> ContextC.insert_assumptions pres;
    1.53      val ist = Istate.e_pstate
    1.54 @@ -307,24 +307,24 @@
    1.55      val p' = Ctree.par_pblobj pt p
    1.56  	  val metID = Ctree.get_obj Ctree.g_metID pt p'
    1.57  	  val ctxt = Ctree.get_ctxt pt pos
    1.58 -	  val {srls, ...} = MethodC.from_store_PIDE ctxt metID
    1.59 +	  val {srls, ...} = MethodC.from_store ctxt metID
    1.60    in srls end
    1.61  
    1.62  (* resume program interpretation at the beginning of a step *)
    1.63 -fun resume_prog_PIDE pos pt =
    1.64 +fun resume_prog pos pt =
    1.65    let
    1.66 -    val (is_problem, p', rls', ctxt) = parent_node_PIDE pt pos (*is Ctree.PrfObj in case of detail step*)
    1.67 +    val (is_problem, p', rls', ctxt) = parent_node pt pos (*is Ctree.PrfObj in case of detail step*)
    1.68    in
    1.69      if is_problem then
    1.70        let
    1.71  	      val metID = get_obj g_metID pt p'
    1.72 -	      val {srls, ...} = MethodC.from_store_PIDE ctxt metID
    1.73 +	      val {srls, ...} = MethodC.from_store ctxt metID
    1.74  	      val (is, ctxt) =
    1.75  	        case get_loc pt pos of
    1.76  	           (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
    1.77  	        | _ => raise ERROR "resume_prog: unexpected result from get_loc"
    1.78  	    in
    1.79 -	      ((is, ctxt), (#scr o MethodC.from_store_PIDE ctxt) metID)
    1.80 +	      ((is, ctxt), (#scr o MethodC.from_store ctxt) metID)
    1.81  	    end
    1.82      else
    1.83        (get_loc pt pos,