diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/Term8.thy
--- a/Nominal/Ex/Term8.thy	Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/Term8.thy	Mon May 10 15:45:04 2010 +0200
@@ -2,22 +2,27 @@
 imports "../NewParser"
 begin
 
-(* example 8 from Terms.thy *)
+(* example 8 *)
 
 atom_decl name
 
+(* this should work but gives an error at the moment:
+   seems like in the symmetry proof
+*)
+
 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
+| Bar1 "name" s::"name" b::"bar" bind s in b
 binder
   bv
 where
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
+
 end