1.1 --- a/src/Tools/isac/Interpret/generate.sml	Wed Dec 21 11:27:22 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 10:25:49 2016 +0100
     1.3 @@ -1,9 +1,12 @@
     1.4 -(* use"ME/generate.sml";
     1.5 -   use"generate.sml";
     1.6 -   *)
     1.7 +(* Title: generate specific entries into Ctree
     1.8 +   Author: Walther Neuper
     1.9 +   (c) due to copyright terms
    1.10 +*)
    1.11 +
    1.12  signature GENERATE_CALC_TREE =
    1.13 -sig (*vvv request into signature is incremental with *.sml *)
    1.14 -  (* for calchead.sml --------------------------------------------------------------  vvv *)
    1.15 +sig
    1.16 +  (* vvv request into signature is incremental with *.sml *)
    1.17 +  (* for calchead.sml ---------------------------------------------------------------  vvv *)
    1.18    type taci
    1.19    val e_taci : taci
    1.20    datatype pblmet = Method of metID | Problem of pblID | Upblmet
    1.21 @@ -13,18 +16,18 @@
    1.22    | FormKF of cterm'
    1.23    | PpcKF of pblmet * item ppc
    1.24    | RefinedKF of pblID * (itm list * (bool * term) list)
    1.25 -  val generate1 : theory -> tac_ -> istate * Proof.context ->
    1.26 -    pos' -> ptree -> pos' * pos' list * mout * ptree (* for calchead.sml ^^^ *)
    1.27 -  val init_istate : tac -> term -> istate (* for solve.sml *)
    1.28 +  val generate1 : theory -> Ctree.tac_ -> Ctree.istate * Proof.context ->
    1.29 +    Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree (* for calchead.sml------------- ^^^ *)
    1.30 +  val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *)
    1.31    val init_pbl : (string * (term * 'a)) list -> itm list
    1.32    val init_pbl' : (string * (term * term)) list -> itm list
    1.33 -  val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos') (* for inform.sml *)
    1.34 +  val embed_deriv : taci list -> Ctree.ptree * Ctree.pos' -> Ctree.pos' list * (Ctree.ptree * Ctree.pos') (* for inform.sml *)
    1.35    val generate_hard : (* for solve.sml *)
    1.36 -    theory -> tac_ -> pos' -> ptree -> pos' * pos' list * mout * ptree
    1.37 -  val generate : (tac * tac_ * (pos' * (istate * Proof.context))) list ->
    1.38 -    ptree * pos' list * pos' -> ptree * pos' list * pos' (* for mathengine.sml *)
    1.39 -  val generate_inconsistent_rew : subs option * thm'' -> term -> istate * Proof.context ->
    1.40 -    pos' -> ptree -> ptree * pos' (* for interface.sml *)
    1.41 +    theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree
    1.42 +  val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list ->
    1.43 +    Ctree.ptree * Ctree.pos' list * Ctree.pos' -> Ctree.ptree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
    1.44 +  val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context ->
    1.45 +    Ctree.pos' -> Ctree.ptree -> Ctree.ptree * Ctree.pos' (* for interface.sml *)
    1.46  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.47  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.48  end
    1.49 @@ -33,6 +36,7 @@
    1.50  structure Generate(**): GENERATE_CALC_TREE(**) =
    1.51  (**)
    1.52  struct
    1.53 +open Ctree
    1.54  (* initialize istate for Detail_Set *)
    1.55  fun init_istate (Rewrite_Set rls) t =
    1.56      (case assoc_rls rls of