1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sat Feb 04 11:21:56 2023 +0100
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Sat Feb 04 16:20:45 2023 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term -> 
     1.5        Program.leaf * term option
     1.6  
     1.7 -  val implicit_take: Program.T -> Env.T -> term option
     1.8 +  val implicit_take: Proof.context -> Program.T -> Env.T -> term option
     1.9    val get_simplifier: Calc.T -> Rule_Set.T
    1.10    val tac_from_prog: Ctree.state -> term -> Tactic.input
    1.11  (*from isac_test for Minisubpbl*)
    1.12 @@ -44,9 +44,9 @@
    1.13  open Pos
    1.14  
    1.15  (* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
    1.16 -fun implicit_take (Rule.Prog prog) env =
    1.17 +fun implicit_take ctxt (Rule.Prog prog) env =
    1.18      Option.map (subst_atomic env) (Prog_Tac.get_first_argument prog)
    1.19 -  | implicit_take _ _ = raise ERROR "implicit_take: no match";
    1.20 +  | implicit_take _ _ _ = raise ERROR "implicit_take: no match";
    1.21  
    1.22  (*  *)
    1.23  val error_msg_1 = "ERROR: the guard is missing (#model in 'type met' added in prep_met)."