--- a/Nominal/Abs.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/Abs.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -1,5 +1,5 @@
 theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Quotient" "Quotient_Product"
 begin
 
 lemma permute_boolI:
@@ -272,8 +272,6 @@
   apply(simp)
   done
 
-term "alpha_abs_tst"
-
 quotient_type ('a,'b) abs_tst = "(('a \<Rightarrow>atom set) \<times> 'a::pt \<times> 'b::pt)" / "alpha_abs_tst"
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
@@ -299,7 +297,6 @@
   apply(simp)
   done
 
-
 quotient_definition
   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
 is