Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;

--- a/src/Pure/Isar/local_theory.ML	Thu Nov 19 13:00:16 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Nov 19 14:44:22 2009 +0100
@@ -32,7 +32,7 @@
   val pretty: local_theory -> Pretty.T list
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
-  val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+  val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -63,8 +63,7 @@
  {pretty: local_theory -> Pretty.T list,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
-  define: string ->
-    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+  define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -185,11 +184,12 @@
 (* basic operations *)
 
 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
+fun operation1 f x = operation (fn ops => f ops x);
 fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
 
 val pretty = operation #pretty;
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
-val define = apsnd checkpoint ooo operation2 #define;
+val define = apsnd checkpoint oo operation1 #define;
 val notes_kind = apsnd checkpoint ooo operation2 #notes;
 val type_syntax = checkpoint ooo operation2 #type_syntax;
 val term_syntax = checkpoint ooo operation2 #term_syntax;

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