--- a/src/HOL/Tools/recdef_package.ML Wed Oct 18 23:58:07 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML Thu Oct 19 01:47:50 2000 +0200
@@ -12,6 +12,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 tcs_of: theory -> xstring -> term list
val simp_add_global: theory attribute
val simp_del_global: theory attribute
val cong_add_global: theory attribute
@@ -138,6 +139,14 @@
val map_global_hints = GlobalRecdefData.map o apsnd;
+fun tcs_of thy raw_name =
+ let val name = Sign.intern_const (Theory.sign_of thy) raw_name in
+ (case get_recdef thy name of
+ None => error ("No recdef definition of constant: " ^ quote name)
+ | Some {tcs, ...} => tcs)
+ end;
+
+
(* proof data kind 'HOL/recdef' *)
structure LocalRecdefArgs =