# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272984156 -7200
# Node ID 5aa5c87f7fc039e60fefe6cc03c3c20d3ffe8c8d
# Parent  232595afb82e9e52d7c67c46055e4d87b854efdf# Parent  a58c73e394791d9be7ef65ad9d1c884d90f2dfda
merge

diff -r 232595afb82e -r 5aa5c87f7fc0 Nominal/Ex/Ex1rec.thy
--- a/Nominal/Ex/Ex1rec.thy	Tue May 04 16:42:28 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy	Tue May 04 16:42:36 2010 +0200
@@ -1,22 +1,22 @@
 theory Ex1rec
-imports "../Parser" 
+imports "../NewParser"
 begin
 
 atom_decl name
 
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaGen *}
+ML {* val _ = cheat_supp_eq := true *}
+
 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
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" t::"lam"  bind_set x in t
+| Let bp::"bp" t::"lam"   bind_set "bi bp" in bp t
 and bp =
-  BP "name" "lam"
+  Bp "name" "lam"
 binder
   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]
@@ -25,8 +25,9 @@
 thm lam_bp.induct
 thm lam_bp.inducts
 thm lam_bp.distinct
+thm lam_bp.supp
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-thm lam_bp.fv[simplified lam_bp.supp]
+thm lam_bp.fv[simplified lam_bp.supp(1-2)]
 
 end