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