# HG changeset patch
# User wenzelm
# Date 1333464545 -7200
# Node ID 052cd5f1a591d0e546833889b9f9af59546ddf73
# Parent  1884d34e9aabba4d43cca51eb793ce06ee0c95ee
another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);

diff -r 1884d34e9aab -r 052cd5f1a591 src/Pure/Isar/generic_target.ML
--- 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;