another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);

--- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 16:27:32 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 16:49:05 2012 +0200
@@ -311,7 +311,7 @@
         Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs))
   #-> (fn lhs => fn lthy' => lthy' |>
         const_declaration (fn level => level <> Local_Theory.level lthy') prmode
-          ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+          ((b, if null xs then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
 fun theory_declaration decl =
   background_declaration decl #> standard_declaration (K true) decl;