diff -r 72bed4519c86 -r 4444d52201dc Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu Apr 29 16:16:45 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Apr 29 16:18:38 2010 +0200
@@ -470,11 +470,11 @@
 nominal_datatype exp =
   EVar name
 | EUnit
-| EPair q1::exp q2::exp      bind_set q1 q2 in q1 q2
+| EPair q1::exp q2::exp
 | ELetRec l::lrbs e::exp     bind "b_lrbs l" in e l
 
 and fnclause =
-  K x::name p::pat f::exp    bind_res "b_pat p" in f 
+  K x::name p::pat f::exp    bind_res "b_pat p" in f
 
 and fnclauses =
   S fnclause
@@ -493,31 +493,37 @@
 | PPair pat pat
 
 binder
-  b_lrbs      :: "lrbs \<Rightarrow> atom set" and
+  b_lrbs      :: "lrbs \<Rightarrow> atom list" and
   b_pat       :: "pat \<Rightarrow> atom set" and
-  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
-  b_fnclause  :: "fnclause \<Rightarrow> atom set" and
-  b_lrb       :: "lrb \<Rightarrow> atom set"
+  b_fnclauses :: "fnclauses \<Rightarrow> atom list" and
+  b_fnclause  :: "fnclause \<Rightarrow> atom list" and
+  b_lrb       :: "lrb \<Rightarrow> atom list"
 
 where
   "b_lrbs (Single l) = b_lrb l"
-| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
+| "b_lrbs (More l ls) = append (b_lrb l) (b_lrbs ls)"
 | "b_pat (PVar x) = {atom x}"
 | "b_pat (PUnit) = {}"
 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
 | "b_fnclauses (S fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
+| "b_fnclauses (ORs fc fcs) = append (b_fnclause fc) (b_fnclauses fcs)"
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp) = {atom x}"
+| "b_fnclause (K x pat exp) = [atom x]"
 
-
-typ exp_raw 
-typ pat_raw 
+typ exp_raw
+typ pat_raw
 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
 
+nominal_datatype ty =
+  Var "name"
+| Fun "ty" "ty"
+
+nominal_datatype tys =
+  All xs::"name fset" ty::"ty_raw" bind_res xs in ty
+thm fv_tys_raw.simps
 
 (* some further tests *)
 
@@ -526,12 +532,6 @@
 | App2 "lam2" "lam2 list"
 | Lam2 x::"name" t::"lam2" bind x in t
 
-nominal_datatype ty =
-  Var "name"
-| Fun "ty" "ty"
-
-nominal_datatype tys =
-  All xs::"name fset" ty::"ty_raw" bind xs in ty