# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272889871 -7200
# Node ID 7f504136149b6f6aac0d0905b2bd68f299a451a0
# Parent  070ba8972e97ca2b93b58d5a43dc59a8c08a73c0
Another example where only alpha_eqvt fails.

diff -r 070ba8972e97 -r 7f504136149b Nominal/Ex/Ex2.thy
--- a/Nominal/Ex/Ex2.thy	Mon May 03 14:30:37 2010 +0200
+++ b/Nominal/Ex/Ex2.thy	Mon May 03 14:31:11 2010 +0200
@@ -1,35 +1,33 @@
 theory Ex2
-imports "../Parser"
+imports "../NewParser"
 begin
 
 text {* example 2 *}
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
-nominal_datatype trm' =
+ML {* val _ = cheat_alpha_eqvt := true *}
+
+nominal_datatype trm =
   Var "name"
-| App "trm'" "trm'"
-| Lam x::"name" t::"trm'"          bind x in t
-| Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
-and pat' =
+| App "trm" "trm"
+| Lam x::"name" t::"trm"          bind_set x in t
+| Let p::"pat" "trm" t::"trm"   bind_set "f p" in t
+and pat =
   PN
 | PS "name"
 | PD "name" "name"
 binder
-  f::"pat' \<Rightarrow> atom set"
+  f::"pat \<Rightarrow> atom set"
 where
   "f PN = {}"
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
-
-thm trm'_pat'.fv
-thm trm'_pat'.eq_iff
-thm trm'_pat'.bn
-thm trm'_pat'.perm
-thm trm'_pat'.induct
-thm trm'_pat'.distinct
-thm trm'_pat'.fv[simplified trm'_pat'.supp]
+thm trm_pat.bn
+thm trm_pat.perm
+thm trm_pat.induct
+thm trm_pat.distinct
+thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
 end