--- a/Nominal/Parser.thy	Thu Mar 11 11:15:14 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 11:20:50 2010 +0100
@@ -271,6 +271,7 @@
 
 ML {* val restricted_nominal=ref 0 *}
 ML {* val cheat_alpha_eqvt = ref true *}
+ML {* val cheat_fv_eqvt = ref true *}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -324,15 +325,17 @@
   val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
+  val fv_eqvt_tac =
+    if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
+    else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
+  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
+  val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
+  val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
 in
 if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
 else
 let
-  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc
-    (build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5) lthy5;
-  val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
-  val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
     inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;