# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 54b09e82b9e1f8841aeb641e66432fd7a3fc0f74
# Parent  b742489618193243ff15e1fb14f95e03c26002f3
killed 'rep_compat' option

diff -r b74248961819 -r 54b09e82b9e1 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -470,7 +470,7 @@
   @@{command datatype_new} target? @{syntax dt_options}? \<newline>
     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
   ;
-  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
+  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code') + ',') ')'
 \<close>}
 
 \medskip
@@ -492,12 +492,6 @@
 \item
 The @{text "no_code"} option indicates that the datatype should not be
 registered for code generation.
-
-\item
-The @{text "rep_compat"} option indicates that the generated names should
-contain optional (and normally not displayed) ``@{text "new."}'' components to
-prevent clashes with a later call to \keyw{rep\_datatype}. See
-Section~\ref{ssec:datatype-compatibility-issues} for details.
 \end{itemize}
 
 The left-hand sides of the datatype equations specify the name of the type to
@@ -2563,7 +2557,7 @@
 %    old \keyw{datatype}
 %
 %  * @{command wrap_free_constructors}
-%    * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"}
+%    * @{text "no_discs_sels"}, @{text "no_code"}
 %    * hack to have both co and nonco view via locale (cf. ext nats)
 %  * code generator
 %     * eq, refl, simps
@@ -2601,7 +2595,7 @@
 
 \medskip
 
-% options: no_discs_sels no_code rep_compat
+% options: no_discs_sels no_code
 
 \noindent
 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
diff -r b74248961819 -r 54b09e82b9e1 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -95,7 +95,7 @@
   val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
-    (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
+    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
       * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
         mixfix) list) list ->
     local_theory -> local_theory
@@ -978,7 +978,7 @@
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
-    (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 =
+    (wrap_opts as (no_discs_sels, _), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
 
@@ -987,9 +987,6 @@
       else
         ();
 
-    fun qualify mandatory fp_b_name =
-      Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
-
     val nn = length specs;
     val fp_bs = map type_binding_of specs;
     val fp_b_names = map Binding.name_of fp_bs;
@@ -1041,7 +1038,7 @@
 
     val disc_bindingss = map (map disc_of) ctr_specss;
     val ctr_bindingss =
-      map2 (fn fp_b_name => map (qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
+      map2 (fn fp_b_name => map (Binding.qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss;
     val ctr_argsss = map (map args_of) ctr_specss;
     val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
 
@@ -1150,12 +1147,12 @@
     fun massage_simple_notes base =
       filter_out (null o #2)
       #> map (fn (thmN, thms, attrs) =>
-        ((qualify true base (Binding.name thmN), attrs), [(thms, [])]));
+        ((Binding.qualify true base (Binding.name thmN), attrs), [(thms, [])]));
 
     val massage_multi_notes =
       maps (fn (thmN, thmss, attrs) =>
         map3 (fn fp_b_name => fn Type (T_name, _) => fn thms =>
-            ((qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])]))
+            ((Binding.qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])]))
           fp_b_names fpTs thmss)
       #> filter_out (null o fst o hd o snd);
 
@@ -1346,7 +1343,7 @@
                lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
             end;
 
-        fun mk_binding pre = qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
+        fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
 
         fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
           (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);
diff -r b74248961819 -r 54b09e82b9e1 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -41,8 +41,6 @@
   val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
   val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
 
-  val rep_compat_prefix: string
-
   val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
   val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
 
@@ -56,10 +54,10 @@
     (ctr_sugar * term list * term list) option
 
   val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
-    (((bool * (bool * bool)) * term list) * binding) *
+    (((bool * bool) * term list) * binding) *
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     ctr_sugar * local_theory
-  val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser
+  val parse_wrap_free_constructors_options: (bool * bool) parser
   val parse_bound_term: (binding * string) parser
 end;
 
@@ -153,8 +151,6 @@
 fun register_ctr_sugar_global key ctr_sugar =
   Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
 
-val rep_compat_prefix = "new";
-
 val isN = "is_";
 val unN = "un_";
 fun mk_unN 1 1 suf = unN ^ suf
@@ -282,7 +278,7 @@
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
-fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs),
+fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs),
     raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -300,8 +296,7 @@
     val fc_b_name = Long_Name.base_name fcT_name;
     val fc_b = Binding.name fc_b_name;
 
-    fun qualify mandatory =
-      Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
+    fun qualify mandatory = Binding.qualify mandatory fc_b_name;
 
     fun dest_TFree_or_TVar (TFree sS) = sS
       | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
@@ -929,8 +924,7 @@
       in
         (ctr_sugar,
          lthy
-         |> not rep_compat ?
-            Local_Theory.declaration {syntax = false, pervasive = true}
+         |> Local_Theory.declaration {syntax = false, pervasive = true}
               (fn phi => Case_Translation.register
                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
          |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
@@ -967,10 +961,10 @@
 
 val parse_wrap_free_constructors_options =
   Scan.optional (@{keyword "("} |-- Parse.list1
-        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 ||
-         Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"}
-      >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2))))
-    (false, (false, false));
+        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
+      @{keyword ")"}
+      >> (fn js => (member (op =) js 0, member (op =) js 1)))
+    (false, false);
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}