1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Thu Dec 08 10:33:27 2022 +0100
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Thu Dec 08 17:55:45 2022 +0100
     1.3 @@ -300,7 +300,7 @@
     1.4    | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
     1.5      let
     1.6        val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
     1.7 -        (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
     1.8 +        (Tactic.Rewrite_Inst (Subst.T_to_input ctxt subs', thm')) (f',asm) Ctree.Complete;
     1.9        val pt = Ctree.update_branch pt p Ctree.TransitiveB
    1.10      in
    1.11        ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
    1.12 @@ -315,7 +315,7 @@
    1.13    | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
    1.14      let
    1.15        val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 
    1.16 -        (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
    1.17 +        (Tactic.Rewrite_Set_Inst (Subst.T_to_input ctxt subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
    1.18        val pt = Ctree.update_branch pt p Ctree.TransitiveB
    1.19      in
    1.20        ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)