diff -r 0913f697fe73 -r d33781f9d2c7 Nominal/Ex/ExPS8.thy
--- a/Nominal/Ex/ExPS8.thy	Fri Apr 23 11:12:38 2010 +0200
+++ b/Nominal/Ex/ExPS8.thy	Sat Apr 24 09:49:23 2010 +0200
@@ -11,41 +11,41 @@
    the reference.  *)
 ML {* val _ = recursive := false  *}
 
-nominal_datatype exp8 =
+nominal_datatype exp =
   EVar name
 | EUnit
-| EPair exp8 exp8
-| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)
+| EPair exp exp
+| ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *)
 and fnclause =
-  K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)
+  K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *)
 and fnclauses =
   S fnclause
 | ORs fnclause fnclauses
-and lrb8 =
+and lrb =
   Clause fnclauses
-and lrbs8 =
-  Single lrb8
-| More lrb8 lrbs8
-and pat8 =
+and lrbs =
+  Single lrb
+| More lrb lrbs
+and pat =
   PVar name
 | PUnit
-| PPair pat8 pat8
+| PPair pat pat
 binder
-  b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
-  b_pat :: "pat8 \<Rightarrow> atom set" and
+  b_lrbs :: "lrbs \<Rightarrow> atom set" and
+  b_pat :: "pat \<Rightarrow> atom set" and
   b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
   b_fnclause :: "fnclause \<Rightarrow> atom set" and
-  b_lrb8 :: "lrb8 \<Rightarrow> atom set"
+  b_lrb :: "lrb \<Rightarrow> atom set"
 where
-  "b_lrbs8 (Single l) = b_lrb8 l"
-| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
+  "b_lrbs (Single l) = b_lrb l"
+| "b_lrbs (More l ls) = b_lrb l \<union> 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_lrb8 (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp8) = {atom x}"
+| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K x pat exp) = {atom x}"
 
 thm exp7_lrb_lrbs.eq_iff
 thm exp7_lrb_lrbs.supp