--- a/Quot/Nominal/LFex.thy	Wed Feb 24 10:47:41 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 10:59:31 2010 +0100
@@ -1,5 +1,5 @@
 theory LFex
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
 begin
 
 atom_decl name
@@ -70,75 +70,28 @@
      @{thms alpha_eqvt} ctxt)) ctxt)) *}
 thm alpha_equivps
 
-quotient_type kind = rkind / alpha_rkind
-  by (rule alpha_equivps)
-
-quotient_type
-    ty = rty / alpha_rty and
-    trm = rtrm / alpha_rtrm
-  by (auto intro: alpha_equivps)
-
-quotient_definition
-   "TYP :: kind"
-is
-  "Type"
-
-quotient_definition
-   "KPI :: ty \<Rightarrow> name \<Rightarrow> kind \<Rightarrow> kind"
-is
-  "KPi"
-
-quotient_definition
-   "TCONST :: ident \<Rightarrow> ty"
-is
-  "TConst"
-
-quotient_definition
-   "TAPP :: ty \<Rightarrow> trm \<Rightarrow> ty"
-is
-  "TApp"
-
-quotient_definition
-   "TPI :: ty \<Rightarrow> name \<Rightarrow> ty \<Rightarrow> ty"
-is
-  "TPi"
+local_setup  {* define_quotient_type
+  [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})),
+   (([], @{binding ty},   NoSyn), (@{typ rty},   @{term alpha_rty}  )),
+   (([], @{binding trm},  NoSyn), (@{typ rtrm},  @{term alpha_rtrm} ))]
+  (ALLGOALS (resolve_tac @{thms alpha_equivps}))
+*}
 
-(* FIXME: does not work with CONST *)
-quotient_definition
-   "CONS :: ident \<Rightarrow> trm"
-is
-  "Const"
-
-quotient_definition
-   "VAR :: name \<Rightarrow> trm"
-is
-  "Var"
-
-quotient_definition
-   "APP :: trm \<Rightarrow> trm \<Rightarrow> trm"
-is
-  "App"
-
-quotient_definition
-   "LAM :: ty \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"
-is
-  "Lam"
-
-(* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *)
-quotient_definition
-   "fv_kind :: kind \<Rightarrow> atom set"
-is
-  "fv_rkind"
-
-quotient_definition
-   "fv_ty :: ty \<Rightarrow> atom set"
-is
-  "fv_rty"
-
-quotient_definition
-   "fv_trm :: trm \<Rightarrow> atom set"
-is
-  "fv_rtrm"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type}))
+ |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi}))
+ |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst}))
+ |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp}))
+ |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi}))
+ |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const}))
+ |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var}))
+ |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App}))
+ |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}
+print_theorems
 
 lemma alpha_rfv:
   shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and>