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;