1.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Tue Dec 20 08:11:26 2022 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Wed Dec 21 18:48:23 2022 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4    type single
     1.5    val single_empty : single
     1.6    type T
     1.7 -  val to_string : T -> string
     1.8 +  val to_string : Proof.context -> T -> string
     1.9    val result : single -> (term * term list)
    1.10    val make_single: Rewrite_Ord.id * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
    1.11      single
    1.12 @@ -37,13 +37,13 @@
    1.13     (Pos.pos' *                        (* after applying tac_, for ctree generation *)
    1.14      (Istate_Def.T * Proof.context)))  (* after applying tac_, for ctree generation *)
    1.15  val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
    1.16 -fun taci2str ((tac, tac_, (pos', (istate, _))):single) =
    1.17 -  "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
    1.18 +fun taci2str ctxt ((tac, tac_, (pos', (istate, _))): single) =
    1.19 +  "( " ^ Tactic.input_to_string ctxt tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
    1.20    Istate_Def.string_of istate ^ " ))"
    1.21  
    1.22  type T = single list;
    1.23  
    1.24 -fun to_string tacis = (strs2str o (map (linefeed o taci2str))) tacis
    1.25 +fun to_string ctxt tacis = (strs2str o (map (linefeed o (taci2str ctxt)))) tacis
    1.26  fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
    1.27    | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
    1.28    | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)