1.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Sat May 02 16:55:14 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Sat May 02 17:39:04 2020 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    val to_string : T -> string
     1.5    val result : single -> (term * term list)
     1.6    val make_single: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
     1.7 -    Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))
     1.8 +    single
     1.9    val insert_pos : Pos.pos -> T -> T
    1.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.11    (* NONE *)