# HG changeset patch
# User bulwahn
# Date 1264079601 -3600
# Node ID fac9d03117252f50f24ae2cbc9c62bbe76b85270
# Parent  57b1eebf7e6cce9b8b0054b792f59fd912f504e8
corrected and simplified Spec_Rules registration in the Recdef package

diff -r 57b1eebf7e6c -r fac9d0311725 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Thu Jan 21 12:20:28 2010 +0100
+++ b/src/HOL/Tools/recdef.ML	Thu Jan 21 14:13:21 2010 +0100
@@ -204,18 +204,13 @@
     val simp_att =
       if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]
       else [];
-    fun specs_of simps =
-      let
-        fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
-        val ts = distinct (op =) (map dest_eqn simps)
-      in (ts, simps) end
     val ((simps' :: rules', [induct']), thy) =
       thy
       |> Sign.add_path bname
       |> PureThy.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
-      ||> Spec_Rules.add_global Spec_Rules.Equational (specs_of (flat rules));
+      ||> Spec_Rules.add_global Spec_Rules.Equational (tcs, flat rules);
     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
       thy