diff -r ee68ccda7977 -r 56762e8a672e src/Tools/isac/Interpret/mathengine.sml
--- a/src/Tools/isac/Interpret/mathengine.sml	Mon Dec 12 18:08:13 2016 +0100
+++ b/src/Tools/isac/Interpret/mathengine.sml	Wed Dec 14 09:37:01 2016 +0100
@@ -9,11 +9,11 @@
 signature MATH_ENGINE =
 sig
   type NEW (* TODO: refactor "fun me" with calcstate and remove *)
-  val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * mout * tac'_ * safe * ptree
+  val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Ctree.mout * tac'_ * safe * ptree
   val autocalc :
-     pos' list -> pos' -> (ptree * pos') * taci list -> auto -> string * pos' list * (ptree * pos')
+     pos' list -> pos' -> (ptree * pos') * Ctree.taci list -> auto -> string * pos' list * (ptree * pos')
   val locatetac :
-    tac -> ptree * (posel list * pos_) -> string * (taci list * pos' list * (ptree * pos'))
+    tac -> ptree * (posel list * pos_) -> string * (Ctree.taci list * pos' list * (ptree * pos'))
   val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
   val detailstep :
     ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
@@ -30,8 +30,8 @@
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
   type nxt_
   type lOc_
-  val CalcTreeTEST : fmz list -> pos' * NEW * mout * (string * tac) * safe * ptree
-  val f2str : mout -> cterm'
+  val CalcTreeTEST : fmz list -> pos' * NEW * Ctree.mout * (string * tac) * safe * ptree
+  val f2str : Ctree.mout -> cterm'
   val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
 end
@@ -62,7 +62,7 @@
   let
     val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
   in
-    case f of (Error' (Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
+    case f of (Ctree.Error' (Ctree.Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
   end
 
 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
@@ -195,7 +195,7 @@
         (_::_) => 
           if ip = p (*the request is done where ptp waits for*)
           then 
-            let val (pt',c',p') = generate tacis (pt,[],p)
+            let val (pt',c',p') = Ctree.generate tacis (pt,[],p)
   	        in ("ok", (tacis, c', (pt', p'))) end
           else (case (if member op = [Pbl, Met] p_
   	                  then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
@@ -368,10 +368,10 @@
     val (form, _, _) = Chead.pt_extract ptp
   in
     case form of
-      Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
+      Form t => Ctree.Form' (Ctree.FormKF (~1,Ctree.EdUndef,0,Ctree.Nundef,term2str t))
     | ModSpec (_,p_, _, gfr, pre, _) => 
-      Form' (PpcKF (0, EdUndef, 0, Nundef, 
-        (case p_ of Pbl => Problem [] | Met => Method [] | _ => error "TESTg_form: uncovered case",
+      Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, 0, Ctree.Nundef, 
+        (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method [] | _ => error "TESTg_form: uncovered case",
  			itms2itemppc (assoc_thy"Isac") gfr pre)))
    end;
 
@@ -421,6 +421,6 @@
   end
 
 (* for quick test-print-out, until 'type inout' is removed *)
-fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
+fun f2str (Ctree.Form' (Ctree.FormKF (_, _, _, _, cterm'))) = cterm';
 
 end