# HG changeset patch
# User wenzelm
# Date 1258638356 -3600
# Node ID 47b5db0976469d7b75b282e1c6628717b0372a62
# Parent  7bcefaab8d41691832517fa1298021fea09ba701
Specification.definition: Thm.definitionK marks exactly the high-level end-user result;

diff -r 7bcefaab8d41 -r 47b5db097646 src/Pure/Isar/specification.ML
--- 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]);