--- a/Nominal/Ex/Term8.thy	Sun Aug 29 12:17:25 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory Term8
-imports "../NewParser"
-begin
-
-(* example 8 *)
-
-atom_decl name
-
-nominal_datatype foo =
-  Foo0 "name"
-| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f
-and bar =
-  Bar0 "name"
-| Bar1 "name" s::"name" b::"bar" bind (set) s in b
-binder
-  bv
-where
-  "bv (Bar0 x) = {}"
-| "bv (Bar1 v x b) = {atom v}"
-
-(*
-thm foo_bar.supp
-*)
-
-end
-
-