1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Mon Dec 12 18:08:13 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed Dec 14 09:37:01 2016 +0100
     1.3 @@ -9,11 +9,11 @@
     1.4  signature MATH_ENGINE =
     1.5  sig
     1.6    type NEW (* TODO: refactor "fun me" with calcstate and remove *)
     1.7 -  val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * mout * tac'_ * safe * ptree
     1.8 +  val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Ctree.mout * tac'_ * safe * ptree
     1.9    val autocalc :
    1.10 -     pos' list -> pos' -> (ptree * pos') * taci list -> auto -> string * pos' list * (ptree * pos')
    1.11 +     pos' list -> pos' -> (ptree * pos') * Ctree.taci list -> auto -> string * pos' list * (ptree * pos')
    1.12    val locatetac :
    1.13 -    tac -> ptree * (posel list * pos_) -> string * (taci list * pos' list * (ptree * pos'))
    1.14 +    tac -> ptree * (posel list * pos_) -> string * (Ctree.taci list * pos' list * (ptree * pos'))
    1.15    val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
    1.16    val detailstep :
    1.17      ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
    1.18 @@ -30,8 +30,8 @@
    1.19  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.20    type nxt_
    1.21    type lOc_
    1.22 -  val CalcTreeTEST : fmz list -> pos' * NEW * mout * (string * tac) * safe * ptree
    1.23 -  val f2str : mout -> cterm'
    1.24 +  val CalcTreeTEST : fmz list -> pos' * NEW * Ctree.mout * (string * tac) * safe * ptree
    1.25 +  val f2str : Ctree.mout -> cterm'
    1.26    val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
    1.27  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.28  end
    1.29 @@ -62,7 +62,7 @@
    1.30    let
    1.31      val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
    1.32    in
    1.33 -    case f of (Error' (Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
    1.34 +    case f of (Ctree.Error' (Ctree.Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
    1.35    end
    1.36  
    1.37  (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
    1.38 @@ -195,7 +195,7 @@
    1.39          (_::_) => 
    1.40            if ip = p (*the request is done where ptp waits for*)
    1.41            then 
    1.42 -            let val (pt',c',p') = generate tacis (pt,[],p)
    1.43 +            let val (pt',c',p') = Ctree.generate tacis (pt,[],p)
    1.44    	        in ("ok", (tacis, c', (pt', p'))) end
    1.45            else (case (if member op = [Pbl, Met] p_
    1.46    	                  then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
    1.47 @@ -368,10 +368,10 @@
    1.48      val (form, _, _) = Chead.pt_extract ptp
    1.49    in
    1.50      case form of
    1.51 -      Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
    1.52 +      Form t => Ctree.Form' (Ctree.FormKF (~1,Ctree.EdUndef,0,Ctree.Nundef,term2str t))
    1.53      | ModSpec (_,p_, _, gfr, pre, _) => 
    1.54 -      Form' (PpcKF (0, EdUndef, 0, Nundef, 
    1.55 -        (case p_ of Pbl => Problem [] | Met => Method [] | _ => error "TESTg_form: uncovered case",
    1.56 +      Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, 0, Ctree.Nundef, 
    1.57 +        (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method [] | _ => error "TESTg_form: uncovered case",
    1.58   			itms2itemppc (assoc_thy"Isac") gfr pre)))
    1.59     end;
    1.60  
    1.61 @@ -421,6 +421,6 @@
    1.62    end
    1.63  
    1.64  (* for quick test-print-out, until 'type inout' is removed *)
    1.65 -fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
    1.66 +fun f2str (Ctree.Form' (Ctree.FormKF (_, _, _, _, cterm'))) = cterm';
    1.67  
    1.68  end