--- 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;
--- 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))
--- 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];
--- 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