1.1 --- a/src/HOL/Tools/ctr_sugar.ML	Thu Dec 05 13:38:20 2013 +0100
     1.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Thu Dec 05 14:11:45 2013 +0100
     1.3 @@ -448,6 +448,8 @@
     1.4          let
     1.5            fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
     1.6  
     1.7 +          fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
     1.8 +
     1.9            fun alternate_disc k =
    1.10              Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
    1.11  
    1.12 @@ -460,7 +462,7 @@
    1.13                  | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy)
    1.14                | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
    1.15  
    1.16 -          fun sel_rhs b proto_sels =
    1.17 +          fun sel_spec b proto_sels =
    1.18              let
    1.19                val _ =
    1.20                  (case duplicates (op =) (map fst proto_sels) of
    1.21 @@ -475,7 +477,8 @@
    1.22                      quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
    1.23                      ^ quote (Syntax.string_of_typ lthy T')));
    1.24              in
    1.25 -              Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T)
    1.26 +              mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u,
    1.27 +                Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
    1.28              end;
    1.29  
    1.30            val sel_bindings = flat sel_bindingss;
    1.31 @@ -498,18 +501,18 @@
    1.32            val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
    1.33              lthy
    1.34              |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
    1.35 -                let val rhs = Term.lambda u exist_xs_u_eq_ctr in
    1.36 -                  if Binding.is_empty b then
    1.37 -                    if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
    1.38 -                    else pair (alternate_disc k, alternate_disc_no_def)
    1.39 -                  else if Binding.eq_name (b, equal_binding) then
    1.40 -                    pair (rhs, Thm.reflexive (certify lthy rhs))
    1.41 -                  else
    1.42 -                    Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd
    1.43 -                end) ks exist_xs_u_eq_ctrs disc_bindings
    1.44 +                if Binding.is_empty b then
    1.45 +                  if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
    1.46 +                  else pair (alternate_disc k, alternate_disc_no_def)
    1.47 +                else if Binding.eq_name (b, equal_binding) then
    1.48 +                  pair (Term.lambda u exist_xs_u_eq_ctr, refl)
    1.49 +                else
    1.50 +                  Specification.definition (SOME (b, NONE, NoSyn),
    1.51 +                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
    1.52 +              ks exist_xs_u_eq_ctrs disc_bindings
    1.53              ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
    1.54 -              Local_Theory.define ((b, NoSyn),
    1.55 -                ((Thm.def_binding b, []), sel_rhs b proto_sels)) #>> apsnd snd) sel_infos
    1.56 +              Specification.definition (SOME (b, NONE, NoSyn),
    1.57 +                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
    1.58              ||> `Local_Theory.restore;
    1.59  
    1.60            val phi = Proof_Context.export_morphism lthy lthy';
    1.61 @@ -668,11 +671,9 @@
    1.62                val vdiscs = map (rapp v) discs;
    1.63                val vselss = map (map (rapp v)) selss;
    1.64  
    1.65 -              fun massage_dest_def def = def RS meta_eq_to_obj_eq RS fun_cong;
    1.66 -
    1.67                fun make_sel_thm xs' case_thm sel_def =
    1.68                  zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
    1.69 -                  (Drule.forall_intr_vars (case_thm RS (massage_dest_def sel_def RS trans)))));
    1.70 +                    (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
    1.71  
    1.72                val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
    1.73  
    1.74 @@ -706,7 +707,7 @@
    1.75                        nth exist_xs_u_eq_ctrs (k - 1));
    1.76                  in
    1.77                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    1.78 -                    mk_alternate_disc_def_tac ctxt k (massage_dest_def (nth disc_defs (2 - k)))
    1.79 +                    mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
    1.80                        (nth distinct_thms (2 - k)) uexhaust_thm)
    1.81                    |> Thm.close_derivation
    1.82                    |> singleton (Proof_Context.export names_lthy lthy)
    1.83 @@ -719,7 +720,7 @@
    1.84                  map2 (fn k => fn def =>
    1.85                    if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
    1.86                    else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
    1.87 -                  else massage_dest_def def) ks disc_defs;
    1.88 +                  else def) ks disc_defs;
    1.89  
    1.90                val discD_thms = map (fn def => def RS iffD1) disc_defs';
    1.91                val discI_thms =