--- 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 =