diff -r ccbcebef56f3 -r bc9ed52bcef5 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 19:24:07 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 19:41:11 2010 +0100
@@ -510,7 +510,7 @@
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
        Free (x, _) => (NONE, env_lookup env x)
-     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), false), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (i, opt_name) =