diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/mathengine.sml
--- a/src/Tools/isac/Interpret/mathengine.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/src/Tools/isac/Interpret/mathengine.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -9,32 +9,32 @@
 signature MATH_ENGINE =
 sig
   type NEW (* TODO: refactor "fun me" with calcstate and remove *)
-  val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ptree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ptree
+  val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ctree
   val autocalc :
-     Ctree.pos' list -> Ctree.pos' -> (Ctree.ptree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ptree * Ctree.pos')
+     Ctree.pos' list -> Ctree.pos' -> (Ctree.ctree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ctree * Ctree.pos')
   val locatetac :
-    Ctree.tac -> Ctree.ptree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos'))
+    Ctree.tac -> Ctree.ctree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos'))
   val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
   val detailstep :
-    Ctree.ptree -> Ctree.pos' -> string * Ctree.ptree * Ctree.pos'
-  val get_pblID : Ctree.ptree * Ctree.pos' -> pblID option
+    Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
+  val get_pblID : Ctree.ctree * Ctree.pos' -> pblID option
 
-  val initcontext_met : Ctree.ptree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list
-  val initcontext_pbl : Ctree.ptree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list
-  val context_met : metID -> Ctree.ptree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list
-  val context_pbl : pblID -> Ctree.ptree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list
-  val set_method : metID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
-  val set_problem : pblID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
-  val set_theory : thyID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
-  val tryrefine : pblID -> Ctree.ptree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list
+  val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list
+  val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list
+  val context_met : metID -> Ctree.ctree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list
+  val context_pbl : pblID -> Ctree.ctree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list
+  val set_method : metID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
+  val set_problem : pblID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
+  val set_theory : thyID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
+  val tryrefine : pblID -> Ctree.ctree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list
 
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   type nxt_
   type lOc_
-  val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ptree
+  val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ctree
   val f2str : Generate.mout -> cterm'
-  val loc_solve_ : string * Ctree.tac_ -> Ctree.ptree *  Ctree.pos' -> lOc_
-  val loc_specify_ : Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
+  val loc_solve_ : string * Ctree.tac_ -> Ctree.ctree *  Ctree.pos' -> lOc_
+  val loc_specify_ : Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
 end