src/Pure/Isar/specification.ML

--- a/src/Pure/Isar/specification.ML	Wed Apr 20 22:57:29 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Apr 21 12:56:27 2011 +0200
@@ -227,7 +227,7 @@
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
 
     val ([(def_name, [th'])], lthy4) = lthy3
-      |> Local_Theory.notes_kind Thm.definitionK
+      |> Local_Theory.notes_kind ""
         [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;