Thm.add_axiom/add_def: return internal name of foundational axiom;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -91,7 +91,7 @@
             val (c, thy') =
               Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
             val cdef = cname ^ "_def"
-            val (ax, thy'') =
+            val ((_, ax), thy'') =
               Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
             val ax' = Drule.export_without_context ax
           in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end

--- a/src/HOL/Tools/typedef.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -117,7 +117,7 @@
 
     val typedef_deps = Term.add_consts A [];
 
-    val (axiom, axiom_thy) = consts_thy
+    val ((axiom_name, axiom), axiom_thy) = consts_thy
       |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
       ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
       ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;

--- a/src/Pure/Isar/class_target.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -333,8 +333,8 @@
     |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
     |> snd
     |> Thm.add_def false false (b_def, def_eq)
-    |>> Thm.varifyT_global
-    |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
+    |>> apsnd Thm.varifyT_global
+    |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
       #> snd
       #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
     |> Sign.add_const_constraint (c', SOME ty')

--- a/src/Pure/Isar/overloading.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -165,8 +165,9 @@
 
 fun declare c_ty = pair (Const c_ty);
 
-fun define checked b (c, t) = Thm.add_def (not checked) true
-  (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
+fun define checked b (c, t) =
+  Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
+  #>> snd;
 
 fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
   #> Local_Theory.target synchronize_syntax

--- a/src/Pure/Isar/specification.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -173,7 +173,7 @@
         fold_map Thm.add_axiom
           (map (apfst (fn a => Binding.map_name (K a) b))
             (PureThy.name_multi (Name.of_binding b) (map subst props)))
-        #>> (fn ths => ((b, atts), [(ths, [])])));
+        #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
 
     (*facts*)
     val (facts, facts_lthy) = axioms_thy

--- a/src/Pure/Isar/theory_target.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -315,7 +315,7 @@
         | NONE =>
             if is_some (Class_Target.instantiation_param lthy b)
             then AxClass.define_overloaded name' (head, rhs')
-            else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')));
+            else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) #>> snd);
     val def = Local_Defs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,

--- a/src/Pure/axclass.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/axclass.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -306,11 +306,11 @@
     |-> (fn const' as Const (c'', _) =>
       Thm.add_def false true
         (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
-      #>> Thm.varifyT_global
-      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
-      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
-      #> snd
-      #> pair (Const (c, T))))
+      #>> apsnd Thm.varifyT_global
+      #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
+        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
+        #> snd
+        #> pair (Const (c, T))))
     ||> Sign.restore_naming thy
   end;
 
@@ -325,7 +325,7 @@
   in
     thy
     |> Thm.add_def false false (b', prop)
-    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
+    |>> (fn (_, thm) =>  Drule.transitive_thm OF [eq, thm])
   end;
 
 
@@ -515,7 +515,7 @@
 
 fun add_axiom (b, prop) =
   Thm.add_axiom (b, prop) #->
-  (fn thm => PureThy.add_thm ((b, Drule.export_without_context thm), []));
+  (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
 
 fun axiomatize prep mk name add raw_args thy =
   let

--- 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;
 
 
 

--- a/src/Pure/pure_thy.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/pure_thy.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -210,7 +210,7 @@
 fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
   let
     val prop = prep thy (b, raw_prop);
-    val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
+    val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
     val thm = def
       |> Thm.forall_intr_frees
       |> Thm.forall_elim_vars 0