diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/script.sml
--- a/src/Tools/isac/Interpret/script.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/src/Tools/isac/Interpret/script.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -8,21 +8,21 @@
 signature LUCAS_INTERPRETER =
 sig
 
-  type step = Ctree.tac_ * Generate.mout * Ctree.ptree * Ctree.pos' * Ctree.pos' list
+  type step = Ctree.tac_ * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
   datatype locate = NotLocatable | Steps of Ctree.istate * step list
   
   val next_tac : (*diss: next-tactic-function*)
-    theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
+    theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
   val locate_gen : (*diss: locate-function*)
-    theory' * rls -> Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
+    theory' * rls -> Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
 
 (* can these functions be local to Lucin or part of LItools ? *)
-  val sel_rules : Ctree.ptree -> Ctree.pos' -> Ctree.tac list 
+  val sel_rules : Ctree.ctree -> Ctree.pos' -> Ctree.tac list 
   val init_form : 'a -> scr -> (term * term) list -> term option
   val tac_2tac : Ctree.tac_ -> Ctree.tac
   val init_scrstate : theory -> itm list -> metID -> Ctree.istate * Proof.context * scr
-  val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ptree -> rls * (Ctree.istate * Proof.context) * scr
-  val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ptree -> 
+  val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ctree -> rls * (Ctree.istate * Proof.context) * scr
+  val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ctree -> 
     rls * (Ctree.istate * Proof.context) * scr
   val rule2thm'' : rule -> thm''
   val rule2rls' : rule -> string
@@ -31,7 +31,7 @@
   datatype asap = Aundef | AssOnly | AssGen
   datatype appy = Appy of Ctree.tac_ * Ctree.scrstate | Napp of env | Skip of term * env
   datatype appy_ = Napp_ | Skip_
-  val appy : theory' * rls -> Ctree.ptree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
+  val appy : theory' * rls -> Ctree.ctree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
   val formal_args : term -> term list
   val get_stac : 'a -> term -> term option 
   val go : loc_ -> term -> term
@@ -40,11 +40,11 @@
   val id_of_scr : term -> string
    val is_spec_pos : Ctree.pos_ -> bool
   val itms2args : 'a -> metID -> itm list -> term list
-  val nstep_up : theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> env -> lrd list -> appy_ -> 
+  val nstep_up : theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> env -> lrd list -> appy_ -> 
     term option -> term -> appy
-  val sel_appl_atomic_tacs : Ctree.ptree -> Ctree.pos' -> Ctree.tac list
-  val stac2tac : Ctree.ptree -> theory -> term -> Ctree.tac
-  val stac2tac_ : Ctree.ptree -> theory -> term -> Ctree.tac * Ctree.tac_
+  val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Ctree.tac list
+  val stac2tac : Ctree.ctree -> theory -> term -> Ctree.tac
+  val stac2tac_ : Ctree.ctree -> theory -> term -> Ctree.tac * Ctree.tac_
   val upd_env_opt : env -> term option * term -> env
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
 end 
@@ -64,9 +64,9 @@
 type step =
     tac_         (*transformed from associated tac                   *)
     * Generate.mout (*result with indentation etc.                      *)
-    * ptree      (*containing node created by tac_ + resp. scrstate  *)
-    * pos'       (*position in ptree; ptree * pos' is the proofstate *)
-    * pos' list; (*of ptree-nodes probably cut (by fst tac_)         *)
+    * ctree      (*containing node created by tac_ + resp. scrstate  *)
+    * pos'       (*position in ctree; ctree * pos' is the proofstate *)
+    * pos' list; (*of ctree-nodes probably cut (by fst tac_)         *)
 
 fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm''
   | rule2thm'' r = error ("rule2thm': not defined for " ^ rule2str r);
@@ -213,7 +213,7 @@
 
 (* convert a script-tac 'stac' to a tactic 'tac';
    if stac is an initac, then convert to a 'tac_' (as required in appy).
-   arg ptree for pushing the thy specified in rootpbl into subpbls    *)
+   arg ctree for pushing the thy specified in rootpbl into subpbls    *)
 fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ Free (thmID, _) $ _ $ _) =
     let
       val tid = (de_esc_underscore o strip_thy) thmID
@@ -295,7 +295,7 @@
    has been changed (see "datatype tac_"); if yes, recalculate result
    TODO.WN120106 recalculate impl.only for Substitute'
 args
-  pt     : ptree for pushing the thy specified in rootpbl into subpbls
+  pt     : ctree for pushing the thy specified in rootpbl into subpbls
   d      : unused (planned for data for comparison)
   tac_   : from user (via applicable_in); to be compared with ...
   stac   : found in Script
@@ -563,8 +563,8 @@
   (step list)    (* list of steps done until associated stac found;
 	                  initiated with the data for doing the 1st step,
                     thus the head holds these data further on,
-		                while the tail holds steps finished (incl.scrstate in ptree) *)
-| NasApp of      (* stac not associated, but applicable, ptree-node generated    *)
+		                while the tail holds steps finished (incl.scrstate in ctree) *)
+| NasApp of      (* stac not associated, but applicable, ctree-node generated    *)
   scrstate * (step list)
 | NasNap of      (* stac not associated, not applicable, nothing generated;
 	                  for distinction in Or, for leaving iterations, leaving Seq,
@@ -789,7 +789,7 @@
 datatype locate =
   Steps of istate (* producing hd of step list (which was latest)
 	                   for next_tac, for reporting Safe|Unsafe to DG  *)
-	   * step       (* (scrstate producing this step is in ptree !)   *) 
+	   * step       (* (scrstate producing this step is in ctree !)   *) 
 		 list         (* locate_gen may produce intermediate steps      *)
 | NotLocatable;   (* no (m Ass m') or (m AssWeak m') found          *)
 
@@ -798,7 +798,7 @@
    or the end of the script
 args
    m   : input by the user, already checked by applicable_in,
-         (to be searched within Or; and _not_ an m doing the step on ptree !)
+         (to be searched within Or; and _not_ an m doing the step on ctree !)
    p,pt: (incl ets) at the time of input
    scr : the script
    d   : canonical simplifier for locating Take, Substitute, Subproblems etc.
@@ -819,7 +819,7 @@
     (case lo rss f (Thm thm) of
 	    [] => NotLocatable
     | rts' => Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
-  | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos') 
+  | locate_gen (thy',srls) (m:tac_) ((pt,p):ctree * pos') 
 	    (scr as Prog (_ $ body),d) (ScrState (E,l,a,v,S,b), ctxt)  = 
     let val thy = assoc_thy thy';
     in case if l = [] orelse (
@@ -1042,7 +1042,7 @@
     	| SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) => 
     	    (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
   	         (Uistate, ctxt), (e_term, Sundef)))                  (*next stac*)
-  | next_tac thy (ptp as (pt, (p, _)):ptree * pos') (sc as Prog (_ $ body)) 
+  | next_tac thy (ptp as (pt, (p, _)):ctree * pos') (sc as Prog (_ $ body)) 
 	    (ScrState (E,l,a,v,s,_), ctxt) =
     (case if l = [] then appy thy ptp E [R] body NONE v
           else nstep_up thy ptp sc E l Skip_ a v of