diff -r 3cf30bb8c6f6 -r e655ea5f0b5f Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 13:44:54 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 14:05:36 2010 +0100
@@ -269,12 +269,13 @@
 end
 *}
 
-ML {* val cheat_alpha_eqvt = ref true *}
-ML {* val cheat_fv_eqvt = ref true *} (* Needed for non-rec *)
+(* These 2 are critical, we don't know how to do it in term5 *)
 ML {* val cheat_fv_rsp = ref true *}
-ML {* val cheat_const_rsp = ref true *}
+ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
 
-ML {* unsuffix "sdf" "aasdf" *}
+(* Fixes for these 2 are known *)
+ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
+ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -490,7 +491,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), false), env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (i, opt_name) =