# HG changeset patch
# User wenzelm
# Date 893841653 -7200
# Node ID ea7d7a65e4e949b84f9b652d5666d6c82c767a1a
# Parent  9c072489a9e7ec8085bbe3360a3908576e955e5d
tuned get_ax (uses ancestry);
added get_def: theory -> xstring -> thm;

diff -r 9c072489a9e7 -r ea7d7a65e4e9 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 29 11:17:14 1998 +0200
+++ b/src/Pure/thm.ML	Wed Apr 29 11:20:53 1998 +0200
@@ -103,6 +103,7 @@
   val strip_shyps       : thm -> thm
   val implies_intr_shyps: thm -> thm
   val get_axiom         : theory -> xstring -> thm
+  val get_def           : theory -> xstring -> thm
   val name_thm          : string * thm -> thm
   val name_of_thm	: thm -> string
   val axioms_of         : theory -> (string * thm) list
@@ -574,25 +575,30 @@
 (*look up the named axiom in the theory*)
 fun get_axiom theory raw_name =
   let
-    val name = Sign.intern (sign_of theory) Theory.axiomK raw_name;
-    fun get_ax [] = raise Match
+    val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name;
+
+    fun get_ax [] = None
       | get_ax (thy :: thys) =
-          let val {sign, axioms, parents, ...} = rep_theory thy
-          in case Symtab.lookup (axioms, name) of
-                Some t => fix_shyps [] []
-                           (Thm {sign_ref = Sign.self_ref sign,
-                                 der = infer_derivs (Axiom name, []),
-                                 maxidx = maxidx_of_term t,
-                                 shyps = [], 
-                                 hyps = [], 
-                                 prop = t})
-              | None => get_ax parents handle Match => get_ax thys
+          let val {sign, axioms, ...} = Theory.rep_theory thy in
+            (case Symtab.lookup (axioms, name) of
+              Some t =>
+                Some (fix_shyps [] []
+                  (Thm {sign_ref = Sign.self_ref sign,
+                    der = infer_derivs (Axiom name, []),
+                    maxidx = maxidx_of_term t,
+                    shyps = [], 
+                    hyps = [], 
+                    prop = t}))
+            | None => get_ax thys)
           end;
   in
-    get_ax [theory] handle Match
-      => raise THEORY ("No axiom " ^ quote name, [theory])
+    (case get_ax (theory :: Theory.ancestors_of theory) of
+      Some thm => thm
+    | None => raise THEORY ("No axiom " ^ quote name, [theory]))
   end;
 
+fun get_def thy name = get_axiom thy (name ^ "_def");
+
 
 (*return additional axioms of this theory node*)
 fun axioms_of thy =