1.1 --- a/src/HOL/Tools/recdef_package.ML	Mon Aug 04 20:19:59 2008 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Mon Aug 04 20:27:37 2008 +0200
     1.3 @@ -23,10 +23,11 @@
     1.4      theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
     1.5    val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
     1.6      -> theory -> theory * {induct_rules: thm}
     1.7 -  val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
     1.8 -    -> theory -> theory * {induct_rules: thm}
     1.9 -  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool -> local_theory -> Proof.state
    1.10 -  val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool -> local_theory -> Proof.state
    1.11 +  val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
    1.12 +  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool ->
    1.13 +    local_theory -> Proof.state
    1.14 +  val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool ->
    1.15 +    local_theory -> Proof.state
    1.16    val setup: theory -> theory
    1.17  end;
    1.18  
    1.19 @@ -229,7 +230,7 @@
    1.20  
    1.21  (** defer_recdef(_i) **)
    1.22  
    1.23 -fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
    1.24 +fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
    1.25    let
    1.26      val name = Sign.intern_const thy raw_name;
    1.27      val bname = Sign.base_name name;
    1.28 @@ -237,8 +238,8 @@
    1.29      val _ = requires_recdef thy;
    1.30      val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
    1.31  
    1.32 -    val (congs, thy1) = thy |> app_thms raw_congs;
    1.33 -    val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
    1.34 +    val congs = eval_thms (ProofContext.init thy) raw_congs;
    1.35 +    val (thy2, induct_rules) = tfl_fn thy congs name eqs;
    1.36      val ([induct_rules'], thy3) =
    1.37        thy2
    1.38        |> Sign.add_path bname
    1.39 @@ -246,8 +247,8 @@
    1.40        ||> Sign.parent_path;
    1.41    in (thy3, {induct_rules = induct_rules'}) end;
    1.42  
    1.43 -val defer_recdef = gen_defer_recdef Tfl.defer IsarCmd.apply_theorems;
    1.44 -val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarCmd.apply_theorems_i;
    1.45 +val defer_recdef = gen_defer_recdef Tfl.defer Attrib.eval_thms;
    1.46 +val defer_recdef_i = gen_defer_recdef Tfl.defer_i (K I);
    1.47  
    1.48  
    1.49