src/HOL/HOLCF/Tools/fixrec.ML
changeset 45592 8baa0b7f3f66
parent 44080 53d95b52954c
child 45787 9fcaf2557c59
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sat Nov 19 17:20:17 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Nov 19 21:18:38 2011 +0100
     1.3 @@ -363,8 +363,7 @@
     1.4      val simps : (Attrib.binding * thm) list list =
     1.5        map (make_simps lthy) (unfold_thms ~~ blocks')
     1.6      fun mk_bind n : Attrib.binding =
     1.7 -     (Binding.qualify true n (Binding.name "simps"),
     1.8 -       [Attrib.internal (K Simplifier.simp_add)])
     1.9 +     (Binding.qualify true n (Binding.name "simps"), @{attributes [simp]})
    1.10      val simps1 : (Attrib.binding * thm list) list =
    1.11        map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps)
    1.12      val simps2 : (Attrib.binding * thm list) list =