--- 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]);