1.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Nov 17 16:40:27 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Mon Nov 21 12:47:02 2016 +0100
     1.3 @@ -27,21 +27,24 @@
     1.4    val rule2thm'' : rule -> thm''
     1.5    val rule2rls' : rule -> string
     1.6  
     1.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     1.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* 
     1.9    datatype asap = Aundef | AssOnly | AssGen
    1.10 +  datatype appy = Appy of tac_ * scrstate | Napp of env | Skip of term * env
    1.11    datatype appy_ = Napp_ | Skip_
    1.12 -  val itms2args : 'a -> metID -> itm list -> term list
    1.13 +  val appy : theory' * rls -> ptree * pos' -> env -> lrd list -> term -> term option -> term -> appy
    1.14 +  val formal_args : term -> term list
    1.15    val get_stac : 'a -> term -> term option 
    1.16 +  val go : loc_ -> term -> term
    1.17    val handle_leaf : string -> theory' -> rls -> env -> term option -> term -> term -> 
    1.18      term option * stacexpr
    1.19 -  val formal_args : term -> term list
    1.20 -  val go : loc_ -> term -> term
    1.21    val id_of_scr : term -> string
    1.22 -  type appy
    1.23 -  val appy : theory' * rls -> ptree * pos' -> env -> lrd list -> term -> term option -> term -> appy
    1.24 -  val sel_appl_atomic_tacs : ptree -> pos' -> tac list
    1.25 +   val is_spec_pos : pos_ -> bool
    1.26 +  val itms2args : 'a -> metID -> itm list -> term list
    1.27    val nstep_up : theory' * rls -> ptree * pos' -> scr -> env -> lrd list -> appy_ -> 
    1.28      term option -> term -> appy
    1.29 +  val sel_appl_atomic_tacs : ptree -> pos' -> tac list
    1.30 +  val stac2tac : ptree -> theory -> term -> tac
    1.31 +  val stac2tac_ : ptree -> theory -> term -> tac * tac_
    1.32    val upd_env_opt : env -> term option * term -> env
    1.33  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.34  end 
    1.35 @@ -50,7 +53,7 @@
    1.36  val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
    1.37  
    1.38  (**)
    1.39 -structure Lucin: LUCAS_INTERPRETER(**) =
    1.40 +structure Lucin(**): LUCAS_INTERPRETER(**) =
    1.41  struct
    1.42  (**)
    1.43  (* data for creating a new node in ctree; designed for use as:
    1.44 @@ -1209,4 +1212,3 @@
    1.45  (**)
    1.46  end
    1.47  (**)
    1.48 -(*open Lucin;*)