# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273497079 -7200
# Node ID c00885a1534d5c8cf2acd5b363dd0c4b0631ce59
# Parent  248bb900727ea3c308c1ef300d8d6503f6c748ed# Parent  e9f089a5cc17a44bee53f000ad061b1833d77ada
merge

diff -r 248bb900727e -r c00885a1534d Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 10 15:09:53 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 10 15:11:19 2010 +0200
@@ -519,13 +519,12 @@
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = warning "Lifting eq-iff";
   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
-  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp
-  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
-  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
-  val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
-  val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
-  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
-  val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
+  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff_simp
+  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
+  val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1;
+  val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0
+  val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1
+  val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val q_dis = map (lift_thm qtys lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;