src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55410 54b09e82b9e1
parent 55409 b74248961819
child 55444 ec73f81e49e7
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -41,8 +41,6 @@
     1.4    val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
     1.5    val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
     1.6  
     1.7 -  val rep_compat_prefix: string
     1.8 -
     1.9    val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    1.10    val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    1.11  
    1.12 @@ -56,10 +54,10 @@
    1.13      (ctr_sugar * term list * term list) option
    1.14  
    1.15    val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    1.16 -    (((bool * (bool * bool)) * term list) * binding) *
    1.17 +    (((bool * bool) * term list) * binding) *
    1.18        (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    1.19      ctr_sugar * local_theory
    1.20 -  val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser
    1.21 +  val parse_wrap_free_constructors_options: (bool * bool) parser
    1.22    val parse_bound_term: (binding * string) parser
    1.23  end;
    1.24  
    1.25 @@ -153,8 +151,6 @@
    1.26  fun register_ctr_sugar_global key ctr_sugar =
    1.27    Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    1.28  
    1.29 -val rep_compat_prefix = "new";
    1.30 -
    1.31  val isN = "is_";
    1.32  val unN = "un_";
    1.33  fun mk_unN 1 1 suf = unN ^ suf
    1.34 @@ -282,7 +278,7 @@
    1.35  
    1.36  fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    1.37  
    1.38 -fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs),
    1.39 +fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, no_code), raw_ctrs),
    1.40      raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    1.41    let
    1.42      (* TODO: sanity checks on arguments *)
    1.43 @@ -300,8 +296,7 @@
    1.44      val fc_b_name = Long_Name.base_name fcT_name;
    1.45      val fc_b = Binding.name fc_b_name;
    1.46  
    1.47 -    fun qualify mandatory =
    1.48 -      Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
    1.49 +    fun qualify mandatory = Binding.qualify mandatory fc_b_name;
    1.50  
    1.51      fun dest_TFree_or_TVar (TFree sS) = sS
    1.52        | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
    1.53 @@ -929,8 +924,7 @@
    1.54        in
    1.55          (ctr_sugar,
    1.56           lthy
    1.57 -         |> not rep_compat ?
    1.58 -            Local_Theory.declaration {syntax = false, pervasive = true}
    1.59 +         |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.60                (fn phi => Case_Translation.register
    1.61                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
    1.62           |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
    1.63 @@ -967,10 +961,10 @@
    1.64  
    1.65  val parse_wrap_free_constructors_options =
    1.66    Scan.optional (@{keyword "("} |-- Parse.list1
    1.67 -        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 ||
    1.68 -         Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"}
    1.69 -      >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2))))
    1.70 -    (false, (false, false));
    1.71 +        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    1.72 +      @{keyword ")"}
    1.73 +      >> (fn js => (member (op =) js 0, member (op =) js 1)))
    1.74 +    (false, false);
    1.75  
    1.76  val _ =
    1.77    Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}