1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed Dec 21 11:27:22 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Dec 22 10:25:49 2016 +0100
     1.3 @@ -8,43 +8,43 @@
     1.4  signature LUCAS_INTERPRETER =
     1.5  sig
     1.6  
     1.7 -  type step = tac_ * Generate.mout * ptree * pos' * pos' list
     1.8 -  datatype locate = NotLocatable | Steps of istate * step list
     1.9 +  type step = Ctree.tac_ * Generate.mout * Ctree.ptree * Ctree.pos' * Ctree.pos' list
    1.10 +  datatype locate = NotLocatable | Steps of Ctree.istate * step list
    1.11    
    1.12    val next_tac : (*diss: next-tactic-function*)
    1.13 -    theory' * rls -> ptree * pos' -> scr -> istate * 'a -> tac_ * (istate * 'a) * (term * safe)
    1.14 +    theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
    1.15    val locate_gen : (*diss: locate-function*)
    1.16 -    theory' * rls -> tac_ -> ptree * pos' -> scr * 'a -> istate * Proof.context -> locate
    1.17 +    theory' * rls -> Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
    1.18  
    1.19  (* can these functions be local to Lucin or part of LItools ? *)
    1.20 -  val sel_rules : ptree -> pos' -> tac list 
    1.21 +  val sel_rules : Ctree.ptree -> Ctree.pos' -> Ctree.tac list 
    1.22    val init_form : 'a -> scr -> (term * term) list -> term option
    1.23 -  val tac_2tac : tac_ -> tac
    1.24 -  val init_scrstate : theory -> itm list -> metID -> istate * Proof.context * scr
    1.25 -  val from_pblobj' : theory' -> pos * pos_ -> ptree -> rls * (istate * Proof.context) * scr
    1.26 -  val from_pblobj_or_detail' : theory' -> pos * pos_ -> ptree -> 
    1.27 -    rls * (istate * Proof.context) * scr
    1.28 +  val tac_2tac : Ctree.tac_ -> Ctree.tac
    1.29 +  val init_scrstate : theory -> itm list -> metID -> Ctree.istate * Proof.context * scr
    1.30 +  val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ptree -> rls * (Ctree.istate * Proof.context) * scr
    1.31 +  val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ptree -> 
    1.32 +    rls * (Ctree.istate * Proof.context) * scr
    1.33    val rule2thm'' : rule -> thm''
    1.34    val rule2rls' : rule -> string
    1.35  
    1.36  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.37    datatype asap = Aundef | AssOnly | AssGen
    1.38 -  datatype appy = Appy of tac_ * scrstate | Napp of env | Skip of term * env
    1.39 +  datatype appy = Appy of Ctree.tac_ * Ctree.scrstate | Napp of env | Skip of term * env
    1.40    datatype appy_ = Napp_ | Skip_
    1.41 -  val appy : theory' * rls -> ptree * pos' -> env -> lrd list -> term -> term option -> term -> appy
    1.42 +  val appy : theory' * rls -> Ctree.ptree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
    1.43    val formal_args : term -> term list
    1.44    val get_stac : 'a -> term -> term option 
    1.45    val go : loc_ -> term -> term
    1.46    val handle_leaf : string -> theory' -> rls -> env -> term option -> term -> term -> 
    1.47      term option * stacexpr
    1.48    val id_of_scr : term -> string
    1.49 -   val is_spec_pos : pos_ -> bool
    1.50 +   val is_spec_pos : Ctree.pos_ -> bool
    1.51    val itms2args : 'a -> metID -> itm list -> term list
    1.52 -  val nstep_up : theory' * rls -> ptree * pos' -> scr -> env -> lrd list -> appy_ -> 
    1.53 +  val nstep_up : theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> env -> lrd list -> appy_ -> 
    1.54      term option -> term -> appy
    1.55 -  val sel_appl_atomic_tacs : ptree -> pos' -> tac list
    1.56 -  val stac2tac : ptree -> theory -> term -> tac
    1.57 -  val stac2tac_ : ptree -> theory -> term -> tac * tac_
    1.58 +  val sel_appl_atomic_tacs : Ctree.ptree -> Ctree.pos' -> Ctree.tac list
    1.59 +  val stac2tac : Ctree.ptree -> theory -> term -> Ctree.tac
    1.60 +  val stac2tac_ : Ctree.ptree -> theory -> term -> Ctree.tac * Ctree.tac_
    1.61    val upd_env_opt : env -> term option * term -> env
    1.62  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.63  end 
    1.64 @@ -55,6 +55,8 @@
    1.65  (**)
    1.66  structure Lucin(**): LUCAS_INTERPRETER(**) =
    1.67  struct
    1.68 +open Ctree
    1.69 +
    1.70  (**)
    1.71  (* data for creating a new node in ctree; designed for use as:
    1.72     fun ass* scrstate steps = / ... case ass* scrstate steps of /