diff -r 0028571ade2d -r 0e4649095739 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Aug 10 14:06:38 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Aug 10 14:11:28 2010 +0200
@@ -30,9 +30,6 @@
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
   val global_morphism: local_theory -> morphism
-  val pretty: local_theory -> Pretty.T list
-  val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
-    (term * 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
@@ -40,8 +37,11 @@
     local_theory -> (string * thm list) list * local_theory
   val notes_kind: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
+  val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
+    (term * term) * local_theory
   val declaration: bool -> declaration -> local_theory -> local_theory
   val syntax_declaration: bool -> declaration -> local_theory -> local_theory
+  val pretty: local_theory -> Pretty.T list
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
@@ -65,16 +65,16 @@
 (* type lthy *)
 
 type operations =
- {pretty: local_theory -> Pretty.T list,
-  abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
-    (term * term) * local_theory,
-  define: (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 ->
     local_theory -> (string * thm list) list * local_theory,
+  abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
+    (term * term) * local_theory,
   declaration: bool -> declaration -> local_theory -> local_theory,
   syntax_declaration: bool -> declaration -> local_theory -> local_theory,
+  pretty: local_theory -> Pretty.T list,
   reinit: local_theory -> local_theory,
   exit: local_theory -> Proof.context};