src/HOL/Tools/primrec.ML

--- a/src/HOL/Tools/primrec.ML	Thu Nov 19 14:45:56 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Thu Nov 19 14:46:33 2009 +0100
@@ -259,7 +259,7 @@
     val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
   in
     lthy
-    |> fold_map (Local_Theory.define Thm.definitionK) defs
+    |> fold_map Local_Theory.define defs
     |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
   end;