# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272176286 -7200
# Node ID 3395e87d94b8d4da56a03cd03d42829a535b61e9
# Parent  93e5a31ba230d7f31fce0885201503a4db8aad55
tuned and made to compile

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
 
diff -r 93e5a31ba230 -r 3395e87d94b8 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Sun Apr 25 08:06:43 2010 +0200
+++ b/Nominal/Parser.thy	Sun Apr 25 08:18:06 2010 +0200
@@ -665,51 +665,6 @@
 end
 *}
 
-atom_decl name
-
-nominal_datatype exp =
-  EVar name
-| EUnit
-| EPair exp exp
-| ELetRec l::lrbs e::exp     bind "b_lrbs l" in e
-
-and fnclause =
-  K x::name p::pat f::exp    bind "b_pat p" in f 
-
-and fnclauses =
-  S fnclause
-| ORs fnclause fnclauses
-
-and lrb =
-  Clause fnclauses
-
-and lrbs =
-  Single lrb
-| More lrb lrbs
-
-and pat =
-  PVar name
-| PUnit
-| PPair pat pat
-
-binder
-  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_lrb       :: "lrb \<Rightarrow> atom set"
-
-where
-  "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_lrb (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp) = {atom x}"
-
 
 end