# HG changeset patch
# User haftmann
# Date 1281360050 -7200
# Node ID e0ad785031860767f19971b5808e38ea5d278481
# Parent  067d7297671e66499be651bf2dc58dfa9570fcc6
more convenient order

diff -r 067d7297671e -r e0ad78503186 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Aug 09 15:19:45 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Aug 09 15:20:50 2010 +0200
@@ -195,6 +195,33 @@
   end;
 
 
+(* consts in locales *)
+
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
+  let
+    val b' = Morphism.binding phi b;
+    val rhs' = Morphism.term phi rhs;
+    val arg = (b', Term.close_schematic_term rhs');
+    val same_shape = Term.aconv_untyped (rhs, rhs');
+    (* FIXME workaround based on educated guess *)
+    val prefix' = Binding.prefix_of b';
+    val is_canonical_class = is_class andalso
+      (Binding.eq_name (b, b')
+        andalso not (null prefix')
+        andalso List.last prefix' = (Class_Target.class_prefix target, false)
+      orelse same_shape);
+  in
+    not is_canonical_class ?
+      (Context.mapping_result
+        (Sign.add_abbrev Print_Mode.internal arg)
+        (ProofContext.add_abbrev Print_Mode.internal arg)
+      #-> (fn (lhs' as Const (d, _), _) =>
+          same_shape ?
+            (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
+             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
+  end;
+
+
 (* mixfix notation *)
 
 local
@@ -222,33 +249,6 @@
 end;
 
 
-(* consts *)
-
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
-  let
-    val b' = Morphism.binding phi b;
-    val rhs' = Morphism.term phi rhs;
-    val arg = (b', Term.close_schematic_term rhs');
-    val same_shape = Term.aconv_untyped (rhs, rhs');
-    (* FIXME workaround based on educated guess *)
-    val prefix' = Binding.prefix_of b';
-    val is_canonical_class = is_class andalso
-      (Binding.eq_name (b, b')
-        andalso not (null prefix')
-        andalso List.last prefix' = (Class_Target.class_prefix target, false)
-      orelse same_shape);
-  in
-    not is_canonical_class ?
-      (Context.mapping_result
-        (Sign.add_abbrev Print_Mode.internal arg)
-        (ProofContext.add_abbrev Print_Mode.internal arg)
-      #-> (fn (lhs' as Const (d, _), _) =>
-          same_shape ?
-            (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
-             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
-  end;
-
-
 (* abbrev *)
 
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =