1.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Tue Aug 16 15:53:20 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Sun Aug 21 11:22:04 2022 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  type single = 
     1.5    (Tactic.input *                     (* for comparison with input tac             *)      
     1.6     Tactic.T *                         (* for ctree generation                      *)
     1.7 -   (Pos.pos' *                            (* after applying tac_, for ctree generation *)
     1.8 +   (Pos.pos' *                        (* after applying tac_, for ctree generation *)
     1.9      (Istate_Def.T * Proof.context)))  (* after applying tac_, for ctree generation *)
    1.10  val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
    1.11  fun taci2str ((tac, tac_, (pos', (istate, _))):single) =