1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sat Mar 07 18:44:31 2020 +0100
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Tue Mar 10 13:25:00 2020 +0100
     1.3 @@ -12,7 +12,8 @@
     1.4    val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term) -> ass
     1.5    
     1.6    val init_form : 'a -> Program.T -> (term * term) list -> term option
     1.7 -  val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Program.T
     1.8 +  val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID ->
     1.9 +    Istate.T * Proof.context * Program.T
    1.10  
    1.11    val get_simplifier : Calc.T -> Rule.rls
    1.12  (*vvv initialise : Rule.theory'(*?!?*) -> Calc.T -> (Istate.T * Proof.context) * Program.T*)
    1.13 @@ -23,7 +24,7 @@
    1.14    val check_leaf : string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term -> 
    1.15        Program.leaf * term option
    1.16  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.17 -  val de_esc_underscore: string -> string
    1.18 +  (*NONE*)
    1.19  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.20    val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
    1.21  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.22 @@ -38,17 +39,13 @@
    1.23  (**)
    1.24  open Ctree
    1.25  open Pos
    1.26 -(*TODO open Celem for L,R,D;
    1.27 -  the few other Celem.items are acceptable: metID, e_metID, assoc_thy, metID2str, thm''*)
    1.28  
    1.29 -fun de_esc_underscore str =
    1.30 -  let
    1.31 -    fun scan [] = []
    1.32 -    | scan (s :: ss) = if s = "'" then (scan ss) else (s :: (scan ss))
    1.33 -  in (implode o scan o Symbol.explode) str end;
    1.34 -
    1.35 -fun init_form thy (Rule.Prog sc) env =
    1.36 -    (case Prog_Tac.get_first thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
    1.37 +(* determine the first tactic in case of a program with one argument (like simplification)
    1.38 +  and without an initial Tactic.Take *)
    1.39 +fun init_form thy (Rule.Prog prog) env =
    1.40 +    (case Prog_Tac.get_first thy prog of
    1.41 +      NONE => NONE 
    1.42 +    | SOME prog_tac => SOME (subst_atomic env prog_tac))
    1.43    | init_form _ _ _ = error "init_form: no match";
    1.44  
    1.45  type dsc = typ; (* <-> nam..unknow in Descript.thy *)