diff -r 93e5a31ba230 -r 3395e87d94b8 Nominal/Ex/Ex1rec.thy
--- a/Nominal/Ex/Ex1rec.thy	Sun Apr 25 08:06:43 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy	Sun Apr 25 08:18:06 2010 +0200
@@ -6,27 +6,27 @@
 
 ML {* val _ = recursive := true *}
 ML {* val _ = alpha_type := AlphaGen *}
-nominal_datatype lam' =
-  VAR' "name"
-| APP' "lam'" "lam'"
-| LAM' x::"name" t::"lam'"  bind x in t
-| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
-and bp' =
-  BP' "name" "lam'"
+nominal_datatype lam =
+  VAR "name"
+| APP "lam" "lam"
+| LAM x::"name" t::"lam"  bind x in t
+| LET bp::"bp" t::"lam"   bind "bi bp" in t
+and bp =
+  BP "name" "lam"
 binder
-  bi'::"bp' \<Rightarrow> atom set"
+  bi::"bp \<Rightarrow> atom set"
 where
-  "bi' (BP' x t) = {atom x}"
+  "bi (BP x t) = {atom x}"
 
-thm lam'_bp'.fv
-thm lam'_bp'.eq_iff[no_vars]
-thm lam'_bp'.bn
-thm lam'_bp'.perm
-thm lam'_bp'.induct
-thm lam'_bp'.inducts
-thm lam'_bp'.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
-thm lam'_bp'.fv[simplified lam'_bp'.supp]
+thm lam_bp.fv
+thm lam_bp.eq_iff[no_vars]
+thm lam_bp.bn
+thm lam_bp.perm
+thm lam_bp.induct
+thm lam_bp.inducts
+thm lam_bp.distinct
+ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
+thm lam_bp.fv[simplified lam_bp.supp]
 
 end