src/Pure/more_thm.ML

--- a/src/Pure/more_thm.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/more_thm.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -62,8 +62,8 @@
   val forall_intr_frees: thm -> thm
   val unvarify_global: thm -> thm
   val close_derivation: thm -> thm
-  val add_axiom: binding * term -> theory -> thm * theory
-  val add_def: bool -> bool -> binding * term -> theory -> thm * theory
+  val add_axiom: binding * term -> theory -> (string * thm) * theory
+  val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
   type binding = binding * attribute list
   val empty_binding: binding
   val rule_attribute: (Context.generic -> thm -> thm) -> attribute
@@ -347,31 +347,36 @@
 fun add_axiom (b, prop) thy =
   let
     val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
+
     val _ = Sign.no_vars (Syntax.pp_global thy) prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
+
     val thy' =
       Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
-    val axm' = Thm.axiom thy' (Sign.full_name thy' b');
+    val axm_name = Sign.full_name thy' b';
+    val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (recover, []) axm'
       |> unvarify_global
       |> fold elim_implies of_sorts;
-  in (thm, thy') end;
+  in ((axm_name, thm), thy') end;
 
 fun add_def unchecked overloaded (b, prop) thy =
   let
     val _ = Sign.no_vars (Syntax.pp_global thy) prop;
     val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
     val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
+
     val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
-    val axm' = Thm.axiom thy' (Sign.full_name thy' b);
+    val axm_name = Sign.full_name thy' b;
+    val axm' = Thm.axiom thy' axm_name;
     val thm =
       Thm.instantiate (recover, []) axm'
       |> unvarify_global
       |> fold_rev Thm.implies_intr prems;
-  in (thm, thy') end;
+  in ((axm_name, thm), thy') end;