src/Pure/Isar/theory_target.ML

         else theory_notes kind global_facts local_facts)
     |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts)
   end;
 
 
-(* mixfix notation *)
-
-local
-
-fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
-  if not is_locale then (NoSyn, NoSyn, mx)
-  else if not is_class then (NoSyn, mx, NoSyn)
-  else (mx, NoSyn, NoSyn);
-
-in
-
-fun prep_mixfix ctxt ta (b, extra_tfrees) mx =
-  let
-    val mx' =
-      if null extra_tfrees then mx
-      else
-        (warning
-          ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
-            commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
-            (if mx = NoSyn then ""
-             else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
-          NoSyn);
-  in fork_mixfix ta mx' end;
-
-end;
-
-
-(* consts *)
+(* 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;

       #-> (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
+
+fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
+  if not is_locale then (NoSyn, NoSyn, mx)
+  else if not is_class then (NoSyn, mx, NoSyn)
+  else (mx, NoSyn, NoSyn);
+
+in
+
+fun prep_mixfix ctxt ta (b, extra_tfrees) mx =
+  let
+    val mx' =
+      if null extra_tfrees then mx
+      else
+        (warning
+          ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
+            commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+            (if mx = NoSyn then ""
+             else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx)));
+          NoSyn);
+  in fork_mixfix ta mx' end;
+
+end;
 
 
 (* abbrev *)
 
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =