1.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Nov 14 15:51:10 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Nov 17 16:40:27 2016 +0100
     1.3 @@ -27,7 +27,7 @@
     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_ = Napp_ | Skip_
    1.11    val itms2args : 'a -> metID -> itm list -> term list
    1.12 @@ -43,14 +43,14 @@
    1.13    val nstep_up : theory' * rls -> ptree * pos' -> scr -> env -> lrd list -> appy_ -> 
    1.14      term option -> term -> appy
    1.15    val upd_env_opt : env -> term option * term -> env
    1.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.18  end 
    1.19  
    1.20  (* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)   
    1.21  val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
    1.22  
    1.23  (**)
    1.24 -structure Lucin(*: LUCAS_INTERPRETER*) =
    1.25 +structure Lucin: LUCAS_INTERPRETER(**) =
    1.26  struct
    1.27  (**)
    1.28  (* data for creating a new node in ctree; designed for use as: