# HG changeset patch
# User wenzelm
# Date 1270992135 -7200
# Node ID 2af69e16eced1b83b83ef37cbc32bec6b81cbdcb
# Parent  19deea20035809b8944e6e03bd7dd9729fe5eb05
expose foundational typedef axiom name;

diff -r 19deea200358 -r 2af69e16eced src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Apr 11 14:30:34 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Sun Apr 11 15:22:15 2010 +0200
@@ -8,7 +8,7 @@
 signature TYPEDEF =
 sig
   type info =
-   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} *
+   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
    {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
     Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
     Rep_induct: thm, Abs_induct: thm}
@@ -36,7 +36,7 @@
 
 type info =
   (*global part*)
-  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} *
+  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
   (*local part*)
   {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
     Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
@@ -122,7 +122,7 @@
       ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
       ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
 
-  in ((RepC, AbsC, axiom), axiom_thy) end;
+  in ((RepC, AbsC, axiom_name, axiom), axiom_thy) end;
 
 
 (* prepare_typedef *)
@@ -177,20 +177,20 @@
 
     val typedef_name = Binding.prefix_name "type_definition_" name;
 
-    val ((RepC, AbsC, typedef), typedef_lthy) =
+    val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) =
       let
         val thy = ProofContext.theory_of set_lthy;
         val cert = Thm.cterm_of thy;
         val (defs, A) =
           Local_Defs.export_cterm set_lthy (ProofContext.init thy) (cert set') ||> Thm.term_of;
 
-        val ((RepC, AbsC, axiom), axiom_lthy) = set_lthy |>
+        val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
           Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
 
         val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy);
         val typedef =
           Local_Defs.contract axiom_lthy defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
-      in ((RepC, AbsC, typedef), axiom_lthy) end;
+      in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end;
 
     val alias_lthy = typedef_lthy
       |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
@@ -236,8 +236,8 @@
               make @{thm type_definition.Abs_induct});
 
         val info =
-          ({rep_type = oldT, abs_type = newT,
-            Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC)},
+          ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC),
+            Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name},
            {inhabited = inhabited, type_definition = type_definition, set_def = set_def,
             Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
             Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,