# HG changeset patch
# User wenzelm
# Date 971912870 -7200
# Node ID ca52783f9801dadda05c40c60d46a8ee972e4fbb
# Parent  325ead6d945795024a4b2d830b42407c4e3a4190
added tcs_of;

diff -r 325ead6d9457 -r ca52783f9801 src/HOL/Tools/recdef_package.ML
--- 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 =