--- a/src/Pure/Isar/theory_target.ML Thu Nov 19 13:00:16 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Thu Nov 19 14:44:22 2009 +0100
@@ -270,7 +270,7 @@
(* define *)
-fun define ta kind ((b, mx), ((name, atts), rhs)) lthy =
+fun define ta ((b, mx), ((name, atts), rhs)) lthy =
let
val thy = ProofContext.theory_of lthy;
val thy_ctxt = ProofContext.init thy;
@@ -301,7 +301,7 @@
(*note*)
val ([(res_name, [res])], lthy4) = lthy3
- |> notes ta kind [((name', atts), [([def], [])])];
+ |> notes ta "" [((name', atts), [([def], [])])];
in ((lhs, (res_name, res)), lthy4) end;