--- 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.
--- 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);
--- 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"}