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