# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268303118 -3600
# Node ID 137cad9c1ce9e4b6f5f2f425821c2361f4ea4978
# Parent  6b9833936281ffe12fb3d285d8b791a94e27a705
Equivp working only on the standard alpha-equivalences.

diff -r 6b9833936281 -r 137cad9c1ce9 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 11:20:50 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 11:25:18 2010 +0100
@@ -331,18 +331,18 @@
   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;
+  val alpha_equivp_loc = map (equivp_hack lthy6) (List.take (alpha_ts_loc, length perms))
+(*  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;*)
+  val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
+  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
 in
 if !restricted_nominal = 0 then
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
 else
 let
-  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;
-  val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
-  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))
     (ALLGOALS (resolve_tac alpha_equivp)) lthy6;