diff -r 55b49de0c2c7 -r 04dad9b0136d Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Mar 12 17:42:31 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 13 13:49:15 2010 +0100
@@ -502,6 +502,10 @@
 *}
 
 ML {*
+val recursive = ref false
+*}
+
+ML {*
 fun prepare_binds dt_strs lthy = 
 let
   fun extract_annos_binds dt_strs =
@@ -510,7 +514,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), !recursive), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (i, opt_name) =