# HG changeset patch
# User berghofe
# Date 1188317657 -7200
# Node ID a33258c78ed2b0b45f7ada65abea60be4b2f936e
# Parent  8eb0f4a36d04d4ce32cfe479b0d4990de31e461f
Adapted to changes in interface of Specification.theorem_i

diff -r 8eb0f4a36d04 -r a33258c78ed2 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Aug 28 18:12:00 2007 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue Aug 28 18:14:17 2007 +0200
@@ -26,8 +26,8 @@
     -> theory -> theory * {induct_rules: thm}
   val defer_recdef_i: xstring -> term list -> (thm list * attribute list) list
     -> theory -> theory * {induct_rules: thm}
-  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> local_theory -> Proof.state
-  val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> local_theory -> Proof.state
+  val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> bool -> local_theory -> Proof.state
+  val recdef_tc_i: bstring * Attrib.src list -> string -> int option -> bool -> local_theory -> Proof.state
   val setup: theory -> theory
 end;
 
@@ -257,7 +257,7 @@
 
 (** recdef_tc(_i) **)
 
-fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i lthy =
+fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val name = prep_name thy raw_name;
@@ -272,7 +272,7 @@
         " in recdef definition of " ^ quote name);
   in
     Specification.theorem_i Thm.internalK NONE (K I) (bname, atts)
-      [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) lthy
+      [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;
 
 val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
@@ -322,7 +322,7 @@
     (P.opt_target --
       SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
       >> (fn (((loc, thm_name), name), i) =>
-        Toplevel.print o Toplevel.local_theory_to_proof loc (recdef_tc thm_name name i)));
+        Toplevel.print o Toplevel.local_theory_to_proof' loc (recdef_tc thm_name name i)));
 
 
 val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];