--- a/src/HOL/Tools/old_primrec.ML Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Tools/old_primrec.ML Fri Mar 12 12:14:30 2010 +0100
@@ -281,14 +281,13 @@
thy'
|> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
val simps'' = maps snd simps';
- fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
- val specs = (distinct (op =) (map dest_eqn simps''), simps'')
+ val lhss = map (Logic.varify o fst o Logic.dest_equals o snd) defs';
in
thy''
|> note (("simps",
[Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
|> snd
- |> Spec_Rules.add_global Spec_Rules.Equational specs
+ |> Spec_Rules.add_global Spec_Rules.Equational (lhss, simps)
|> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
|> snd
|> Sign.parent_path