--- a/src/Pure/old_goals.ML Fri Feb 19 17:37:33 2010 +0100
+++ b/src/Pure/old_goals.ML Fri Feb 19 20:39:48 2010 +0100
@@ -16,6 +16,7 @@
val simple_read_term: theory -> typ -> string -> term
val read_term: theory -> string -> term
val read_prop: theory -> string -> term
+ val get_def: theory -> xstring -> thm
type proof
val premises: unit -> thm list
val reset_goals: unit -> unit
@@ -220,6 +221,8 @@
fun read_prop thy = simple_read_term thy propT;
+fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
+
(*** Goal package ***)