diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/generate.sml
--- a/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -17,17 +17,17 @@
   | PpcKF of pblmet * item ppc
   | RefinedKF of pblID * (itm list * (bool * term) list)
   val generate1 : theory -> Ctree.tac_ -> Ctree.istate * Proof.context ->
-    Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree (* for calchead.sml------------- ^^^ *)
+    Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *)
   val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *)
   val init_pbl : (string * (term * 'a)) list -> itm list
   val init_pbl' : (string * (term * term)) list -> itm list
-  val embed_deriv : taci list -> Ctree.ptree * Ctree.pos' -> Ctree.pos' list * (Ctree.ptree * Ctree.pos') (* for inform.sml *)
+  val embed_deriv : taci list -> Ctree.ctree * Ctree.pos' -> Ctree.pos' list * (Ctree.ctree * Ctree.pos') (* for inform.sml *)
   val generate_hard : (* for solve.sml *)
-    theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree
+    theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
   val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list ->
-    Ctree.ptree * Ctree.pos' list * Ctree.pos' -> Ctree.ptree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
+    Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
   val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context ->
-    Ctree.pos' -> Ctree.ptree -> Ctree.ptree * Ctree.pos' (* for interface.sml *)
+    Ctree.pos' -> Ctree.ctree -> Ctree.ctree * Ctree.pos' (* for interface.sml *)
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
 end
@@ -86,9 +86,9 @@
     not any more used for the specify-phase and for changing the phases*)
 type taci = 
   (tac *                        (* for comparison with input tac             *)      
-   tac_ *                       (* for ptree generation                      *)
-   (pos' *                      (* after applying tac_, for ptree generation *)
-    (istate * Proof.context)))  (* after applying tac_, for ptree generation *)
+   tac_ *                       (* for ctree generation                      *)
+   (pos' *                      (* after applying tac_, for ctree generation *)
+    (istate * Proof.context)))  (* after applying tac_, for ctree generation *)
 val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci
 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
   "( " ^ tac2str tac ^ ", " ^ tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
@@ -177,7 +177,7 @@
     fun pbt2itm (f, (d, t)) = ((0, [], false, f, Inc((d, [t]), (e_term, []))) : itm)
   in map pbt2itm pbt end
 
-(*generate 1 ppobj in ptree*)
+(*generate 1 ppobj in ctree*)
 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt = 
     (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]),