diff -r 9e7cf0a996d3 -r 0854af516f14 Nominal/Ex/Term8.thy
--- a/Nominal/Ex/Term8.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/Term8.thy	Sun May 09 12:26:10 2010 +0100
@@ -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