# HG changeset patch
# User wenzelm
# Date 1258638262 -3600
# Node ID 7bcefaab8d41691832517fa1298021fea09ba701
# Parent  b1fbd5f3cfb4e56161861cb111b5b8dbbd367abf
Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;

diff -r b1fbd5f3cfb4 -r 7bcefaab8d41 src/Pure/Isar/local_theory.ML
--- 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;
diff -r b1fbd5f3cfb4 -r 7bcefaab8d41 src/Pure/Isar/theory_target.ML
--- 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;