1.1 --- a/src/Tools/isac/Interpret/derive.sml	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4      	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
     1.5      		(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
     1.6      			(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
     1.7 -    	val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
     1.8 +    	val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
     1.9      	val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
    1.10      	val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
    1.11      	val pt = Ctree.update_branch pt p Ctree.TransitiveB
    1.12 @@ -171,7 +171,7 @@
    1.13      	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
    1.14      		(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), 
    1.15      			(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
    1.16 -    	val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
    1.17 +    	val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
    1.18      	val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
    1.19      	val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
    1.20      	val pt = Ctree.update_branch pt p Ctree.TransitiveB