# HG changeset patch
# User wenzelm
# Date 1350069755 -7200
# Node ID 31f32ec4d766e2f3500ff5bb1cb20cdc8bd4a38e
# Parent  b27bbb021df16be2a7c794aec8e33928510f5a5d
discontinued typedef with alternative name;

diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -625,7 +625,7 @@
     val deads = map TFree params;
 
     val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
-      typedef NONE (bdT_bind, params, NoSyn)
+      typedef (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
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Oct 12 21:22:35 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 NONE (sbdT_bind, dead_params, NoSyn)
+            typedef (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 NONE (b, params, mx) car_final NONE
+        typedef (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;
 
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Oct 12 21:22:35 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 NONE (IIT_bind, params, NoSyn)
+      typedef (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 NONE (b, params, mx) car_init NONE
+      |> fold_map3 (fn b => fn mx => fn car_init => typedef (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;
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Oct 12 21:22:35 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: binding option -> binding * (string * sort) list * mixfix -> term ->
+  val typedef: 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 opt_name typ set opt_morphs tac lthy =
+fun typedef typ set opt_morphs tac lthy =
   let
     val ((name, info), (lthy, lthy_old)) =
       lthy
-      |> Typedef.add_typedef opt_name typ set opt_morphs tac
+      |> Typedef.add_typedef typ set opt_morphs tac
       ||> `Local_Theory.restore;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -168,7 +168,7 @@
   let
     val name = #1 typ
     val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
-      |> Typedef.add_typedef_global NONE typ set opt_morphs tac
+      |> Typedef.add_typedef_global 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))
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/Import/import_rule.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -220,9 +220,8 @@
     val tfrees = Term.add_tfrees c []
     val tnames = sort_strings (map fst tfrees)
     val ((_, typedef_info), thy') =
-     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
+     Typedef.add_typedef_global (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)
     val th = freezeT (#type_definition (#2 typedef_info))
     val (th_s, _) = Thm.dest_comb (Thm.dest_arg (cprop_of th))
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -572,7 +572,7 @@
     val (typedefs, thy6) =
       thy4
       |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
-          Typedef.add_typedef_global NONE
+          Typedef.add_typedef_global
             (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
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -190,7 +190,7 @@
       |> Sign.parent_path
       |> fold_map
         (fn (((name, mx), tvs), c) =>
-          Typedef.add_typedef_global NONE (name, tvs, mx)
+          Typedef.add_typedef_global (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -45,7 +45,7 @@
     val typedef_tac =
       EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
   in
-    Typedef.add_typedef NONE (qty_name, map (rpair dummyS) vs, mx)
+    Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
       (typedef_term rel rty lthy) NONE typedef_tac lthy
   end
 
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/Tools/record.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -112,7 +112,7 @@
     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   in
     thy
-    |> Typedef.add_typedef_global (SOME raw_tyco) (raw_tyco, vs, NoSyn)
+    |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
         (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
diff -r b27bbb021df1 -r 31f32ec4d766 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/Tools/typedef.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -17,13 +17,13 @@
   val get_info_global: theory -> string -> info list
   val interpretation: (string -> theory -> theory) -> theory -> theory
   val setup: theory -> theory
-  val add_typedef: binding option -> binding * (string * sort) list * mixfix ->
+  val add_typedef: binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
-  val add_typedef_global: binding option -> binding * (string * sort) list * mixfix ->
+  val add_typedef_global: binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
-  val typedef: binding * (binding * (string * sort) list * mixfix) * term *
+  val typedef: (binding * (string * sort) list * mixfix) * term *
     (binding * binding) option -> local_theory -> Proof.state
-  val typedef_cmd: binding * (binding * (string * string option) list * mixfix) * string *
+  val typedef_cmd: (binding * (string * string option) list * mixfix) * string *
     (binding * binding) option -> local_theory -> Proof.state
 end;
 
@@ -128,9 +128,8 @@
 
 (* prepare_typedef *)
 
-fun prepare_typedef prep_term name (tname, raw_args, mx) raw_set opt_morphs lthy =
+fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
   let
-    val full_name = Local_Theory.full_name lthy name;
     val bname = Binding.name_of name;
 
 
@@ -152,10 +151,10 @@
 
     val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args;
     val (newT, typedecl_lthy) = lthy
-      |> Typedecl.typedecl (tname, args, mx)
+      |> Typedecl.typedecl (name, args, mx)
       ||> Variable.declare_term set;
 
-    val Type (full_tname, type_args) = newT;
+    val Type (full_name, type_args) = newT;
     val lhs_tfrees = map Term.dest_TFree type_args;
 
 
@@ -203,13 +202,13 @@
                 [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
               make @{thm type_definition.Rep_cases})
           ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name,
-                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
+                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_name]),
               make @{thm type_definition.Abs_cases})
           ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name,
                 [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
               make @{thm type_definition.Rep_induct})
           ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name,
-                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]),
+                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_name]),
               make @{thm type_definition.Abs_induct});
 
         val info =
@@ -222,9 +221,9 @@
       in
         lthy2
         |> Local_Theory.declaration {syntax = false, pervasive = true}
-          (fn phi => put_info full_tname (transform_info phi info))
-        |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
-        |> pair (full_tname, info)
+          (fn phi => put_info full_name (transform_info phi info))
+        |> Local_Theory.background_theory (Typedef_Interpretation.data full_name)
+        |> pair (full_name, info)
       end;
 
   in ((goal, goal_pat, typedef_result), alias_lthy) end
@@ -234,19 +233,18 @@
 
 (* add_typedef: tactic interface *)
 
-fun add_typedef opt_name typ set opt_morphs tac lthy =
+fun add_typedef 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 name typ set opt_morphs lthy;
+      prepare_typedef Syntax.check_term 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 opt_name typ set opt_morphs tac =
+fun add_typedef_global typ set opt_morphs tac =
   Named_Target.theory_init
-  #> add_typedef opt_name typ set opt_morphs tac
+  #> add_typedef typ set opt_morphs tac
   #> Local_Theory.exit_result_global (apsnd o transform_info);
 
 
@@ -254,11 +252,11 @@
 
 local
 
-fun gen_typedef prep_term prep_constraint (name, (b, raw_args, mx), set, opt_morphs) lthy =
+fun gen_typedef prep_term prep_constraint ((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 name (b, args, mx) set opt_morphs lthy;
+      prepare_typedef prep_term (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;
 
@@ -276,12 +274,10 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
     "HOL type definition (requires non-emptiness proof)"
-    (Scan.option (@{keyword "("} |-- Parse.binding --| @{keyword ")"}) --
-      (Parse.type_args_constrained -- Parse.binding) --
-        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
-        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
-    >> (fn (((((opt_name, (args, t)), mx), A), morphs)) => fn lthy =>
-           typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy));
+    (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
+      (@{keyword "="} |-- Parse.term) --
+      Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
+    >> (fn ((((vs, t), mx), A), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy));
 
 end;