--- a/Nominal/Parser.thy	Thu Mar 18 07:26:36 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 07:35:44 2010 +0100
@@ -324,7 +324,7 @@
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
-  val bns = raw_bn_funs ~~ bn_nos;
+  val bns = raw_bn_funs ~~ bn_nos; (* Are exported *)
   val alpha_intros_loc = #intrs alpha;
   val alpha_cases_loc = #elims alpha
   val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc
@@ -335,30 +335,28 @@
   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_nobn fv_eqvt_tac lthy5;
-  val (fv_bn_eqvts, lthy6a) = 
-    if fv_ts_loc_bn = [] then ([], lthy6) else
-    fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) 
-      (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
-  val lthy6 = lthy6a;
-  val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
-  val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy2 raw_fv_bv_eqvt_loc;
+    else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5
+  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5;
+  val (fv_bn_eqvts, lthy6a) =
+    if fv_ts_bn = [] then ([], lthy6) else
+    fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts)
+      (fv_ts_bn ~~ (map snd bns)) lthy6;
+  val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts)
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6 1
-  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
+    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6a 1
+  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a;
   val _ = tracing "Proving equivalence";
   val alpha_equivp =
-    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn
+    if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
     else build_equivps alpha_ts induct alpha_induct
-      inject alpha_inj distincts alpha_cases alpha_eqvt lthy6;
+      inject alpha_inj distincts alpha_cases alpha_eqvt lthy6a;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
   val lthy7 = define_quotient_type
     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
-    (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
+    (ALLGOALS (resolve_tac alpha_equivp)) lthy6a;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>