# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270045677 -7200
# Node ID 6eaae26512927a29d7b97d3ea4e017c6aa365076
# Parent  3832a31a73b19981de1df8886a188c8dafcdb06f# Parent  2293711213dda5325655a3beb3f4dc8e57648e19
merged

diff -r 3832a31a73b1 -r 6eaae2651292 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 31 16:27:44 2010 +0200
+++ b/Paper/Paper.thy	Wed Mar 31 16:27:57 2010 +0200
@@ -1489,10 +1489,13 @@
   obtain by simple calculations the equalities.
   \end{proof}
 
-  With the above equations we can substitute free variables for support in
-  the lifted free variable equations, which gives us the support equations
-  for the term constructors. With this we can show that for each binding in
-  a constructors the bindings can be renamed. 
+%%% Without defining permute_bn, we cannot even write the substitution
+%%% of bindings in term constructors...
+
+% With the above equations we can substitute free variables for support in
+% the lifted free variable equations, which gives us the support equations
+% for the term constructors. With this we can show that for each binding in
+% a constructors the bindings can be renamed.
 
 *}