Specification.definition: Thm.definitionK marks exactly the high-level end-user result;

--- a/src/Pure/Isar/specification.ML	Thu Nov 19 14:44:22 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Nov 19 14:45:56 2009 +0100
@@ -204,8 +204,7 @@
           in (b, mx) end);
     val name = Thm.def_binding_optional b raw_name;
     val ((lhs, (_, raw_th)), lthy2) = lthy
-      |> Local_Theory.define Thm.definitionK
-        (var, ((Binding.suffix_name "_raw" name, []), rhs));
+      |> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs));
 
     val th = prove lthy2 raw_th;
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);