src/Pure/thm.ML

--- a/src/Pure/thm.ML	Tue Mar 31 20:07:37 2015 +0200
+++ b/src/Pure/thm.ML	Tue Mar 31 20:18:10 2015 +0200
@@ -590,8 +590,8 @@
 fun axiom theory name =
   let
     fun get_ax thy =
-      Name_Space.lookup_key (Theory.axiom_table thy) name
-      |> Option.map (fn (_, prop) =>
+      Name_Space.lookup (Theory.axiom_table thy) name
+      |> Option.map (fn prop =>
            let
              val der = deriv_rule0 (Proofterm.axm_proof name prop);
              val maxidx = maxidx_of_term prop;