src/HOL/Tools/recdef_package.ML
changeset 10268 ca52783f9801
parent 10032 1823b34834fd
child 10775 3a5e5657e41c
--- 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 =