# HG changeset patch
# User blanchet
# Date 1392360826 -3600
# Node ID 198498f861eec377a0313b792246af1978814ebd
# Parent  46e6e1d91056f601ccb303203640e3361f4e0c78
more precise spec rules for selectors

diff -r 46e6e1d91056 -r 198498f861ee src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -225,9 +225,6 @@
 
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
-fun lhs_head_of_hd (thm :: _) =
-  [Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))))];
-
 fun flat_rec_arg_args xss =
   (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
      order. The second line is for compatibility with the old datatype package. *)
@@ -1353,9 +1350,9 @@
             in
               (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
                lthy
-               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd map_thms)
-               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd rel_eq_thms)
-               |> Spec_Rules.add Spec_Rules.Equational (`lhs_head_of_hd set_thms)
+               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) map_thms)
+               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) rel_eq_thms)
+               |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) set_thms)
                |> Local_Theory.notes (anonymous_notes @ notes)
                |> snd)
             end;
diff -r 46e6e1d91056 -r 198498f861ee src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -941,8 +941,10 @@
         (ctr_sugar,
          lthy
          |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
-         |> Spec_Rules.add Spec_Rules.Equational (flat selss, all_sel_thms)
-         |> fold (Spec_Rules.add Spec_Rules.Equational) (map single discs ~~ nontriv_disc_eq_thmss)
+         |> fold (Spec_Rules.add Spec_Rules.Equational)
+           (AList.group (eq_list (op aconv)) (map (`lhs_heads_of) all_sel_thms))
+         |> fold (Spec_Rules.add Spec_Rules.Equational)
+           (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
          |> Local_Theory.declaration {syntax = false, pervasive = true}
               (fn phi => Case_Translation.register
                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
diff -r 46e6e1d91056 -r 198498f861ee src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -39,6 +39,8 @@
   val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
   val subst_nonatomic_types: (typ * typ) list -> term -> term
 
+  val lhs_heads_of : thm -> term list
+
   val mk_predT: typ list -> typ
   val mk_pred1T: typ -> typ
 
@@ -168,6 +170,9 @@
 fun subst_nonatomic_types [] = I
   | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst);
 
+fun lhs_heads_of thm =
+  [Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))))];
+
 fun mk_predT Ts = Ts ---> HOLogic.boolT;
 fun mk_pred1T T = mk_predT [T];
 
diff -r 46e6e1d91056 -r 198498f861ee src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Feb 14 07:53:46 2014 +0100
@@ -141,7 +141,7 @@
 
 fun the_pred_data ctxt name =
   (case lookup_pred_data ctxt name of
-    NONE => error ("No such predicate " ^ quote name)  
+    NONE => error ("No such predicate: " ^ quote name)  
   | SOME data => data)
 
 val is_registered = is_some oo lookup_pred_data