1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -14,15 +14,15 @@
     1.4    val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
     1.5    
     1.6    val implicit_take : Program.T -> (term * term) list -> term option
     1.7 -  val init_pstate : Rule_Set.rls -> Proof.context -> Model.itm list -> Celem.metID ->
     1.8 +  val init_pstate : Rule_Set.T -> 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_Set.rls
    1.12 +  val get_simplifier : Calc.T -> Rule_Set.T
    1.13    val resume_prog : Rule.theory' (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree -> 
    1.14      (Istate.T * Proof.context) * Program.T
    1.15  
    1.16    val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input
    1.17 -  val check_leaf : string -> Proof.context -> Rule_Set.rls -> (Env.T * (term option * term)) -> term -> 
    1.18 +  val check_leaf : string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term -> 
    1.19        Program.leaf * term option
    1.20  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.21    (*NONE*)