# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273509170 -7200
# Node ID f81e0f9f2b2eb9eefebe25743f9fe3836d453ea1
# Parent  41c2445fdee4614c0cf52f85a98470defa13b620# Parent  60ce41a111808a653c8194090eac616557c873c2
merge

diff -r 41c2445fdee4 -r f81e0f9f2b2e Nominal/Ex/Term8.thy
--- a/Nominal/Ex/Term8.thy	Mon May 10 18:30:27 2010 +0200
+++ b/Nominal/Ex/Term8.thy	Mon May 10 18:32:50 2010 +0200
@@ -7,7 +7,7 @@
 atom_decl name
 
 (* this should work but gives an error at the moment:
-   seems like in the symmetry proof
+   in alpha_bn_rsp proof.
 *)
 
 nominal_datatype foo =
@@ -15,7 +15,7 @@
 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f
 and bar =
   Bar0 "name"
-| Bar1 "name" s::"name" b::"bar" bind s in b
+| Bar1 "name" s::"name" b::"bar" bind_set s in b
 binder
   bv
 where