# HG changeset patch
# User krauss
# Date 1138872246 -3600
# Node ID 9923269dcf063758e3a1c55796d9603b9a4a5c36
# Parent  34a9e466201fe40b9cb1962d6145cd22e7dc4a3a
Exporting recdef's hints for use by new recdef package

diff -r 34a9e466201f -r 9923269dcf06 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Thu Feb 02 10:12:45 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Thu Feb 02 10:24:06 2006 +0100
@@ -29,6 +29,10 @@
   val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state
   val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
   val setup: theory -> theory
+
+(* HACK: This has to be exported, since the new recdef-package uses the same hints *)
+  val get_local_hints: ProofContext.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
+  val get_global_hints: theory -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
 end;
 
 structure RecdefPackage: RECDEF_PACKAGE =