src/HOL/ex/predicate_compile.ML
changeset 31174 f1f1e9b53c81
parent 31170 c6efe82fc652
child 31177 c39994cb152a
     1.1 --- a/src/HOL/ex/predicate_compile.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -1393,7 +1393,7 @@
     1.4      val (predname, _) = dest_Const pred
     1.5      fun after_qed [[th]] lthy'' =
     1.6        lthy''
     1.7 -      |> LocalTheory.note Thm.theoremK
     1.8 +      |> LocalTheory.note Thm.generated_theoremK
     1.9             ((Binding.empty, [Attrib.internal (K add_elim_attrib)]), [th])
    1.10        |> snd
    1.11        |> LocalTheory.theory (prove_equation predname NONE)