--- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 12 15:08:29 2012 +0200
@@ -625,7 +625,7 @@
val deads = map TFree params;
val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
- typedef false NONE (bdT_bind, params, NoSyn)
+ typedef NONE (bdT_bind, params, NoSyn)
(HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val bnf_bd' = mk_dir_image bnf_bd
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Oct 12 15:08:29 2012 +0200
@@ -1023,7 +1023,7 @@
val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
- typedef false NONE (sbdT_bind, dead_params, NoSyn)
+ typedef NONE (sbdT_bind, dead_params, NoSyn)
(HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val sbdT = Type (sbdT_name, dead_params');
@@ -1824,7 +1824,7 @@
val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
lthy
|> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
- typedef false NONE (b, params, mx) car_final NONE
+ typedef NONE (b, params, mx) car_final NONE
(EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
|>> apsnd split_list o split_list;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Oct 12 15:08:29 2012 +0200
@@ -776,7 +776,7 @@
val IIT_bind = Binding.suffix_name ("_" ^ IITN) b;
val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
- typedef false NONE (IIT_bind, params, NoSyn)
+ typedef NONE (IIT_bind, params, NoSyn)
(HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val IIT = Type (IIT_name, params');
@@ -936,7 +936,7 @@
val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
lthy
- |> fold_map3 (fn b => fn mx => fn car_init => typedef false NONE (b, params, mx) car_init NONE
+ |> fold_map3 (fn b => fn mx => fn car_init => typedef NONE (b, params, mx) car_init NONE
(EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
rtac alg_init_thm] 1)) bs mixfixes car_inits
|>> apsnd split_list o split_list;
--- a/src/HOL/BNF/Tools/bnf_util.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Fri Oct 12 15:08:29 2012 +0200
@@ -154,7 +154,7 @@
val parse_binding_colon: Token.T list -> binding * Token.T list
val parse_opt_binding_colon: Token.T list -> binding * Token.T list
- val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
+ val typedef: binding option -> binding * (string * sort) list * mixfix -> term ->
(binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
@@ -280,11 +280,11 @@
val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
(*TODO: is this really different from Typedef.add_typedef_global?*)
-fun typedef def opt_name typ set opt_morphs tac lthy =
+fun typedef opt_name typ set opt_morphs tac lthy =
let
val ((name, info), (lthy, lthy_old)) =
lthy
- |> Typedef.add_typedef def opt_name typ set opt_morphs tac
+ |> Typedef.add_typedef opt_name typ set opt_morphs tac
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
in
--- a/src/HOL/HOLCF/Tools/cpodef.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Fri Oct 12 15:08:29 2012 +0200
@@ -58,18 +58,6 @@
fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT)
-(* manipulating theorems *)
-
-fun fold_adm_mem thm NONE = thm
- | fold_adm_mem thm (SOME set_def) =
- let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
- in rule OF [set_def, thm] end
-
-fun fold_bottom_mem thm NONE = thm
- | fold_bottom_mem thm (SOME set_def) =
- let val rule = @{lemma "A == B ==> bottom : B ==> bottom : A" by simp}
- in rule OF [set_def, thm] end
-
(* proving class instances *)
fun prove_cpo
@@ -77,14 +65,12 @@
(newT: typ)
(Rep_name: binding, Abs_name: binding)
(type_definition: thm) (* type_definition Rep Abs A *)
- (set_def: thm option) (* A == set *)
(below_def: thm) (* op << == %x y. Rep x << Rep y *)
(admissible: thm) (* adm (%x. x : set) *)
(thy: theory)
=
let
- val admissible' = fold_adm_mem admissible set_def
- val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible']
+ val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible]
val (full_tname, Ts) = dest_Type newT
val lhs_sorts = map (snd o dest_TFree) Ts
val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1
@@ -100,14 +86,14 @@
thy
|> Sign.add_path (Binding.name_of name)
|> Global_Theory.add_thms
- ([((Binding.prefix_name "adm_" name, admissible'), []),
- ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []),
- ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []),
- ((Binding.prefix_name "lub_" name, lub ), []),
- ((Binding.prefix_name "compact_" name, compact ), [])])
+ ([((Binding.prefix_name "adm_" name, admissible), []),
+ ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []),
+ ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []),
+ ((Binding.prefix_name "lub_" name, lub ), []),
+ ((Binding.prefix_name "compact_" name, compact ), [])])
||> Sign.parent_path
val cpo_info : cpo_info =
- { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
+ { below_def = below_def, adm = admissible, cont_Rep = cont_Rep,
cont_Abs = cont_Abs, lub = lub, compact = compact }
in
(cpo_info, thy)
@@ -118,14 +104,12 @@
(newT: typ)
(Rep_name: binding, Abs_name: binding)
(type_definition: thm) (* type_definition Rep Abs A *)
- (set_def: thm option) (* A == set *)
(below_def: thm) (* op << == %x y. Rep x << Rep y *)
(bottom_mem: thm) (* bottom : set *)
(thy: theory)
=
let
- val bottom_mem' = fold_bottom_mem bottom_mem set_def
- val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem']
+ val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem]
val (full_tname, Ts) = dest_Type newT
val lhs_sorts = map (snd o dest_TFree) Ts
val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
@@ -184,7 +168,7 @@
let
val name = #1 typ
val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
- |> Typedef.add_typedef_global false NONE typ set opt_morphs tac
+ |> Typedef.add_typedef_global NONE typ set opt_morphs tac
val oldT = #rep_type (#1 info)
val newT = #abs_type (#1 info)
val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
@@ -222,10 +206,10 @@
fun cpodef_result nonempty admissible thy =
let
- val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
+ val ((info as (_, {type_definition, ...}), below_def), thy) = thy
|> add_podef typ set opt_morphs (Tactic.rtac nonempty 1)
val (cpo_info, thy) = thy
- |> prove_cpo name newT morphs type_definition set_def below_def admissible
+ |> prove_cpo name newT morphs type_definition below_def admissible
in
((info, cpo_info), thy)
end
@@ -256,12 +240,12 @@
fun pcpodef_result bottom_mem admissible thy =
let
val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
- val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
+ val ((info as (_, {type_definition, ...}), below_def), thy) = thy
|> add_podef typ set opt_morphs tac
val (cpo_info, thy) = thy
- |> prove_cpo name newT morphs type_definition set_def below_def admissible
+ |> prove_cpo name newT morphs type_definition below_def admissible
val (pcpo_info, thy) = thy
- |> prove_pcpo name newT morphs type_definition set_def below_def bottom_mem
+ |> prove_pcpo name newT morphs type_definition below_def bottom_mem
in
((info, cpo_info, pcpo_info), thy)
end
--- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Oct 12 15:08:29 2012 +0200
@@ -162,12 +162,8 @@
val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef
val liftprj_def = singleton (Proof_Context.export lthy ctxt_thy) liftprj_ldef
val liftdefl_def = singleton (Proof_Context.export lthy ctxt_thy) liftdefl_ldef
- val type_definition_thm =
- Raw_Simplifier.rewrite_rule
- (the_list (#set_def (#2 info)))
- (#type_definition (#2 info))
val typedef_thms =
- [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def,
+ [#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def,
liftemb_def, liftprj_def, liftdefl_def]
val thy = lthy
|> Class.prove_instantiation_instance
--- a/src/HOL/Import/import_rule.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/Import/import_rule.ML Fri Oct 12 15:08:29 2012 +0200
@@ -220,7 +220,7 @@
val tfrees = Term.add_tfrees c []
val tnames = sort_strings (map fst tfrees)
val ((_, typedef_info), thy') =
- Typedef.add_typedef_global false NONE
+ Typedef.add_typedef_global NONE
(Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
(SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
val aty = #abs_type (#1 typedef_info)
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Oct 12 15:08:29 2012 +0200
@@ -572,7 +572,7 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
- Typedef.add_typedef_global false NONE
+ Typedef.add_typedef_global NONE
(name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
(Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Oct 12 15:08:29 2012 +0200
@@ -190,7 +190,7 @@
|> Sign.parent_path
|> fold_map
(fn (((name, mx), tvs), c) =>
- Typedef.add_typedef_global false NONE (name, tvs, mx)
+ Typedef.add_typedef_global NONE (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 12 15:08:29 2012 +0200
@@ -559,15 +559,13 @@
type typedef_info =
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
- set_def: thm option, prop_of_Rep: thm, set_name: string,
- Abs_inverse: thm option, Rep_inverse: thm option}
+ prop_of_Rep: thm, set_name: string, Abs_inverse: thm option, Rep_inverse: thm option}
fun typedef_info ctxt s =
if is_frac_type ctxt (Type (s, [])) then
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
Abs_name = @{const_name Nitpick.Abs_Frac},
Rep_name = @{const_name Nitpick.Rep_Frac},
- set_def = NONE,
prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"}
|> Logic.varify_global,
set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE,
@@ -579,10 +577,10 @@
types's type variables sometimes clash with locally fixed type variables.
Remove these calls once "Typedef" is fully localized. *)
({abs_type, rep_type, Abs_name, Rep_name, ...},
- {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
+ {Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
SOME {abs_type = Logic.varifyT_global abs_type,
rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name,
- Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
+ Rep_name = Rep_name, prop_of_Rep = prop_of Rep,
set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
Rep_inverse = SOME Rep_inverse}
| _ => NONE
@@ -683,13 +681,10 @@
| is_pure_typedef _ _ = false
fun is_univ_typedef ctxt (Type (s, _)) =
(case typedef_info ctxt s of
- SOME {set_def, prop_of_Rep, ...} =>
+ SOME {prop_of_Rep, ...} =>
let
val t_opt =
- case set_def of
- SOME thm => try (snd o Logic.dest_equals o prop_of) thm
- | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop)
- prop_of_Rep
+ try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) prop_of_Rep
in
case t_opt of
SOME (Const (@{const_name top}, _)) => true
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 15:08:29 2012 +0200
@@ -45,7 +45,7 @@
val typedef_tac =
EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
in
- Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx)
+ Typedef.add_typedef NONE (qty_name, map (rpair dummyS) vs, mx)
(typedef_term rel rty lthy) NONE typedef_tac lthy
end
--- a/src/HOL/Tools/record.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/Tools/record.ML Fri Oct 12 15:08:29 2012 +0200
@@ -112,7 +112,7 @@
val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
in
thy
- |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
+ |> Typedef.add_typedef_global (SOME raw_tyco) (raw_tyco, vs, NoSyn)
(HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
|-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
--- a/src/HOL/Tools/typedef.ML Fri Oct 12 14:05:30 2012 +0200
+++ b/src/HOL/Tools/typedef.ML Fri Oct 12 15:08:29 2012 +0200
@@ -9,21 +9,21 @@
sig
type info =
{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,
+ {inhabited: thm, type_definition: thm, 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}
val transform_info: morphism -> info -> info
val get_info: Proof.context -> string -> info list
val get_info_global: theory -> string -> info list
val interpretation: (string -> theory -> theory) -> theory -> theory
val setup: theory -> theory
- val add_typedef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+ val add_typedef: binding option -> binding * (string * sort) list * mixfix ->
term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
- val add_typedef_global: bool -> binding option -> binding * (string * sort) list * mixfix ->
+ val add_typedef_global: binding option -> binding * (string * sort) list * mixfix ->
term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
- val typedef: (bool * binding) * (binding * (string * sort) list * mixfix) * term *
+ val typedef: binding * (binding * (string * sort) list * mixfix) * term *
(binding * binding) option -> local_theory -> Proof.state
- val typedef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string *
+ val typedef_cmd: binding * (binding * (string * string option) list * mixfix) * string *
(binding * binding) option -> local_theory -> Proof.state
end;
@@ -38,23 +38,22 @@
(*global part*)
{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,
+ {inhabited: thm, type_definition: thm, 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};
fun transform_info phi (info: info) =
let
val thm = Morphism.thm phi;
- val (global_info, {inhabited, type_definition,
- set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
- Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
+ val (global_info, {inhabited, type_definition, Rep, Rep_inverse, Abs_inverse,
+ Rep_inject, Abs_inject, Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
in
(global_info,
{inhabited = thm inhabited, type_definition = thm type_definition,
- set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
- Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
- Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
- Abs_induct = thm Abs_induct})
+ Rep = thm Rep, Rep_inverse = thm Rep_inverse, Abs_inverse = thm Abs_inverse,
+ Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
+ Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases,
+ Rep_induct = thm Rep_induct, Abs_induct = thm Abs_induct})
end;
structure Data = Generic_Data
@@ -129,7 +128,7 @@
(* prepare_typedef *)
-fun prepare_typedef prep_term def_set name (tname, raw_args, mx) raw_set opt_morphs lthy =
+fun prepare_typedef prep_term name (tname, raw_args, mx) raw_set opt_morphs lthy =
let
val full_name = Local_Theory.full_name lthy name;
val bname = Binding.name_of name;
@@ -160,16 +159,6 @@
val lhs_tfrees = map Term.dest_TFree type_args;
- (* set definition *)
-
- val ((set', set_def), set_lthy) =
- if def_set then
- typedecl_lthy
- |> Local_Theory.define ((name, NoSyn), ((Thm.def_binding name, []), set))
- |>> (fn (set', (_, set_def)) => (set', SOME set_def))
- else ((set, NONE), typedecl_lthy);
-
-
(* axiomatization *)
val (Rep_name, Abs_name) =
@@ -179,21 +168,8 @@
val typedef_name = Binding.prefix_name "type_definition_" name;
- val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) =
- let
- val thy = Proof_Context.theory_of set_lthy;
- val cert = Thm.cterm_of thy;
- val ((defs, _), A) =
- Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set')
- ||> Thm.term_of;
-
- val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy
- |> primitive_typedef typedef_name newT oldT Rep_name Abs_name A;
-
- val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy);
- val typedef =
- Local_Defs.contract defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
- in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end;
+ val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
+ |> primitive_typedef typedef_name newT oldT Rep_name Abs_name set;
val alias_lthy = typedef_lthy
|> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
@@ -209,9 +185,7 @@
fun typedef_result inhabited lthy1 =
let
val cert = Thm.cterm_of (Proof_Context.theory_of lthy1);
- val inhabited' =
- Local_Defs.contract (the_list set_def) (cert (mk_inhabited set')) inhabited;
- val typedef' = inhabited' RS typedef;
+ val typedef' = inhabited RS typedef;
fun make th = Goal.norm_result (typedef' RS th);
val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
@@ -241,7 +215,7 @@
val info =
({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,
+ {inhabited = inhabited, type_definition = type_definition,
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
@@ -260,19 +234,19 @@
(* add_typedef: tactic interface *)
-fun add_typedef def opt_name typ set opt_morphs tac lthy =
+fun add_typedef opt_name typ set opt_morphs tac lthy =
let
val name = the_default (#1 typ) opt_name;
val ((goal, _, typedef_result), lthy') =
- prepare_typedef Syntax.check_term def name typ set opt_morphs lthy;
+ prepare_typedef Syntax.check_term name typ set opt_morphs lthy;
val inhabited =
Goal.prove lthy' [] [] goal (K tac)
|> Goal.norm_result |> Thm.close_derivation;
in typedef_result inhabited lthy' end;
-fun add_typedef_global def opt_name typ set opt_morphs tac =
+fun add_typedef_global opt_name typ set opt_morphs tac =
Named_Target.theory_init
- #> add_typedef def opt_name typ set opt_morphs tac
+ #> add_typedef opt_name typ set opt_morphs tac
#> Local_Theory.exit_result_global (apsnd o transform_info);
@@ -280,11 +254,11 @@
local
-fun gen_typedef prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) lthy =
+fun gen_typedef prep_term prep_constraint (name, (b, raw_args, mx), set, opt_morphs) lthy =
let
val args = map (apsnd (prep_constraint lthy)) raw_args;
val ((goal, goal_pat, typedef_result), lthy') =
- prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
+ prepare_typedef prep_term name (b, args, mx) set opt_morphs lthy;
fun after_qed [[th]] = snd o typedef_result th;
in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
@@ -310,9 +284,9 @@
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
>> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
(if def then
- legacy_feature "typedef with implicit set definition -- use \"typedef (open)\" instead"
+ error "typedef with implicit set definition -- use \"typedef (open)\" instead"
else ();
- typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) lthy)));
+ typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy)));
end;