--- a/src/HOL/Tools/recdef.ML Wed Jan 20 14:09:46 2010 +0100
+++ b/src/HOL/Tools/recdef.ML Wed Jan 20 18:02:22 2010 +0100
@@ -204,13 +204,18 @@
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), [])];
+ ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
+ ||> Spec_Rules.add_global Spec_Rules.Equational (specs_of (flat rules));
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy =
thy