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