# HG changeset patch
# User wenzelm
# Date 1154550405 -7200
# Node ID c82b667b6dcc45f7d006bdb88786d7bca447c22c
# Parent  3f886c176c9b46e4f96e9d510f1d5eda327956b2
export get_hints;
tuned;

diff -r 3f886c176c9b -r c82b667b6dcc src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Aug 02 22:26:44 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Wed Aug 02 22:26:45 2006 +0200
@@ -11,6 +11,7 @@
   val print_recdefs: theory -> unit
   val get_recdef: theory -> string
     -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
+  val get_hints: Context.generic -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
   val simp_add: attribute
   val simp_del: attribute
   val cong_add: attribute
@@ -29,10 +30,6 @@
   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 fundef-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 =
@@ -146,11 +143,17 @@
 val map_local_hints = LocalRecdefData.map;
 
 
-(* attributes *)
+(* generic data *)
+
+fun get_hints (Context.Theory thy) = get_global_hints thy
+  | get_hints (Context.Proof ctxt) = get_local_hints ctxt;
 
 fun map_hints f (Context.Theory thy) = Context.Theory (map_global_hints f thy)
   | map_hints f (Context.Proof ctxt) = Context.Proof (map_local_hints f ctxt);
 
+
+(* attributes *)
+
 fun attrib f = Thm.declaration_attribute (map_hints o f);
 
 val simp_add = attrib (map_simps o Drule.add_rule);