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