src/HOL/Tools/old_primrec.ML
changeset 34952 bd7e347eb768
parent 33968 f94fb13ecbb3
child 35756 cfde251d03a5
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Wed Jan 20 14:09:46 2010 +0100
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Wed Jan 20 18:02:22 2010 +0100
     1.3 @@ -281,11 +281,14 @@
     1.4        thy'
     1.5        |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
     1.6      val simps'' = maps snd simps';
     1.7 +    fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
     1.8 +    val specs = (distinct (op =) (map dest_eqn simps''), simps'')
     1.9    in
    1.10      thy''
    1.11      |> note (("simps",
    1.12          [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
    1.13      |> snd
    1.14 +    |> Spec_Rules.add_global Spec_Rules.Equational specs
    1.15      |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
    1.16      |> snd
    1.17      |> Sign.parent_path