1.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Dec 22 11:55:16 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Dec 22 14:05:55 2016 +0100
     1.3 @@ -12,9 +12,9 @@
     1.4    datatype locate = NotLocatable | Steps of Ctree.istate * step list
     1.5    
     1.6    val next_tac : (*diss: next-tactic-function*)
     1.7 -    theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
     1.8 +    theory' * rls -> Ctree.state -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
     1.9    val locate_gen : (*diss: locate-function*)
    1.10 -    theory' * rls -> Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
    1.11 +    theory' * rls -> Ctree.tac_ -> Ctree.state -> scr * 'a -> Ctree.istate * Proof.context -> locate
    1.12  
    1.13  (* can these functions be local to Lucin or part of LItools ? *)
    1.14    val sel_rules : Ctree.ctree -> Ctree.pos' -> Ctree.tac list 
    1.15 @@ -31,7 +31,7 @@
    1.16    datatype asap = Aundef | AssOnly | AssGen
    1.17    datatype appy = Appy of Ctree.tac_ * Ctree.scrstate | Napp of env | Skip of term * env
    1.18    datatype appy_ = Napp_ | Skip_
    1.19 -  val appy : theory' * rls -> Ctree.ctree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
    1.20 +  val appy : theory' * rls -> Ctree.state -> env -> lrd list -> term -> term option -> term -> appy
    1.21    val formal_args : term -> term list
    1.22    val get_stac : 'a -> term -> term option 
    1.23    val go : loc_ -> term -> term
    1.24 @@ -40,7 +40,7 @@
    1.25    val id_of_scr : term -> string
    1.26     val is_spec_pos : Ctree.pos_ -> bool
    1.27    val itms2args : 'a -> metID -> itm list -> term list
    1.28 -  val nstep_up : theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> env -> lrd list -> appy_ -> 
    1.29 +  val nstep_up : theory' * rls -> Ctree.state -> scr -> env -> lrd list -> appy_ -> 
    1.30      term option -> term -> appy
    1.31    val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Ctree.tac list
    1.32    val stac2tac : Ctree.ctree -> theory -> term -> Ctree.tac