1.1 --- a/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 11:12:18 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 11:36:20 2016 +0100
     1.3 @@ -17,17 +17,17 @@
     1.4    | PpcKF of pblmet * item ppc
     1.5    | RefinedKF of pblID * (itm list * (bool * term) list)
     1.6    val generate1 : theory -> Ctree.tac_ -> Ctree.istate * Proof.context ->
     1.7 -    Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree (* for calchead.sml------------- ^^^ *)
     1.8 +    Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *)
     1.9    val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *)
    1.10    val init_pbl : (string * (term * 'a)) list -> itm list
    1.11    val init_pbl' : (string * (term * term)) list -> itm list
    1.12 -  val embed_deriv : taci list -> Ctree.ptree * Ctree.pos' -> Ctree.pos' list * (Ctree.ptree * Ctree.pos') (* for inform.sml *)
    1.13 +  val embed_deriv : taci list -> Ctree.ctree * Ctree.pos' -> Ctree.pos' list * (Ctree.ctree * Ctree.pos') (* for inform.sml *)
    1.14    val generate_hard : (* for solve.sml *)
    1.15 -    theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree
    1.16 +    theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
    1.17    val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list ->
    1.18 -    Ctree.ptree * Ctree.pos' list * Ctree.pos' -> Ctree.ptree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
    1.19 +    Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
    1.20    val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context ->
    1.21 -    Ctree.pos' -> Ctree.ptree -> Ctree.ptree * Ctree.pos' (* for interface.sml *)
    1.22 +    Ctree.pos' -> Ctree.ctree -> Ctree.ctree * Ctree.pos' (* for interface.sml *)
    1.23  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.24  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.25  end
    1.26 @@ -86,9 +86,9 @@
    1.27      not any more used for the specify-phase and for changing the phases*)
    1.28  type taci = 
    1.29    (tac *                        (* for comparison with input tac             *)      
    1.30 -   tac_ *                       (* for ptree generation                      *)
    1.31 -   (pos' *                      (* after applying tac_, for ptree generation *)
    1.32 -    (istate * Proof.context)))  (* after applying tac_, for ptree generation *)
    1.33 +   tac_ *                       (* for ctree generation                      *)
    1.34 +   (pos' *                      (* after applying tac_, for ctree generation *)
    1.35 +    (istate * Proof.context)))  (* after applying tac_, for ctree generation *)
    1.36  val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci
    1.37  fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
    1.38    "( " ^ tac2str tac ^ ", " ^ tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
    1.39 @@ -177,7 +177,7 @@
    1.40      fun pbt2itm (f, (d, t)) = ((0, [], false, f, Inc((d, [t]), (e_term, []))) : itm)
    1.41    in map pbt2itm pbt end
    1.42  
    1.43 -(*generate 1 ppobj in ptree*)
    1.44 +(*generate 1 ppobj in ctree*)
    1.45  (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
    1.46  fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt = 
    1.47      (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]),