diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/inform.sml
--- a/src/Tools/isac/Interpret/inform.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/src/Tools/isac/Interpret/inform.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -10,16 +10,16 @@
   type imodel = iitem list
   type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec
   val fetchErrorpatterns : Ctree.tac -> errpatID list
-  val input_icalhd : Ctree.ptree -> icalhd -> Ctree.ptree * Ctree.ocalhd
+  val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
   val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
-  val find_fillpatterns : Ctree.ptree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
-  val is_exactly_equal : Ctree.ptree * Ctree.pos' -> string -> string * Ctree.tac
+  val find_fillpatterns : Ctree.ctree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
+  val is_exactly_equal : Ctree.ctree * Ctree.pos' -> string -> string * Ctree.tac
 
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
-  val cas_input : term -> (Ctree.ptree * Ctree.ocalhd) option
+  val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
   val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
-  val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos') -> term -> string * Chead.calcstate'
+  val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos') -> term -> string * Chead.calcstate'
   val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
   val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
     rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
@@ -95,7 +95,7 @@
   in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end;
 
 
-(* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *)
+(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
 fun cas_input hdt =
   let
     val (h, argl) = strip_comb hdt
@@ -108,7 +108,7 @@
 	        val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
 	        val spec = (dI, pI, mI)
 	        val (pt,_) = 
-		        Ctree.cappend_problem Ctree.e_ptree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt)
+		        Ctree.cappend_problem Ctree.e_ctree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt)
 	        val pt = Ctree.update_spec pt [] spec
 	        val pt = Ctree.update_pbl pt [] pits
 	        val pt = Ctree.update_met pt [] mits