1.1 --- a/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 11:55:16 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 14:05:55 2016 +0100
     1.3 @@ -21,13 +21,13 @@
     1.4    val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *)
     1.5    val init_pbl : (string * (term * 'a)) list -> itm list
     1.6    val init_pbl' : (string * (term * term)) list -> itm list
     1.7 -  val embed_deriv : taci list -> Ctree.ctree * Ctree.pos' -> Ctree.pos' list * (Ctree.ctree * Ctree.pos') (* for inform.sml *)
     1.8 +  val embed_deriv : taci list -> Ctree.state -> Ctree.pos' list * (Ctree.state) (* for inform.sml *)
     1.9    val generate_hard : (* for solve.sml *)
    1.10      theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
    1.11    val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list ->
    1.12      Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
    1.13    val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context ->
    1.14 -    Ctree.pos' -> Ctree.ctree -> Ctree.ctree * Ctree.pos' (* for interface.sml *)
    1.15 +    Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)
    1.16  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.17  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.18  end