diff -r 6e856be26ac7 -r 947e5f772a9c Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 11:41:27 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 12:26:24 2010 +0100
@@ -271,7 +271,11 @@
 
 ML {* val restricted_nominal=ref 0 *}
 ML {* val cheat_alpha_eqvt = ref true *}
-ML {* val cheat_fv_eqvt = ref true *}
+ML {* val cheat_fv_eqvt = ref true *} (* Needed for non-rec *)
+ML {* val cheat_fv_rsp = ref true *}
+ML {* val cheat_const_rsp = ref true *}
+
+ML {* unsuffix "sdf" "aasdf" *}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
@@ -306,8 +310,10 @@
   val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
+  val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms)
+  val fv_ts_nobn = List.take (fv_ts, length perms)
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
-  val alpha_ts_nobn = List.take (alpha_ts, length perms)
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
   val alpha_induct_loc = #induct alpha
   val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc];
   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
@@ -351,22 +357,20 @@
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
   val (consts, const_defs) = split_list consts_defs;
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
-else
-let
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
       (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
-  val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts
-    (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy9;
-  val (const_rsps, lthy11) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1)) raw_consts lthy10
-  val (perms_rsp, lthy12) = prove_const_rsp Binding.empty perms
-    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy11;
-  val qfv_names = map (fn x => "fv_" ^ x) qty_names
+  fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
+    else fvbv_rsp_tac alpha_induct fv_def 1;
+  val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
+  val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
+    (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+  fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
+    else constr_rsp_tac alpha_inj (fv_rsp @ bns_rsp) alpha_equivp 1
+  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+    const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
+  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts
   val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
@@ -374,6 +378,11 @@
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
+in
+if !restricted_nominal = 0 then
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy13)
+else
+let
   val q_name = space_implode "_" qty_names;
   val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct));
   val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13;
@@ -486,7 +495,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) =