--- a/Paper/Paper.thy	Fri Jul 09 18:50:02 2010 +0100
+++ b/Paper/Paper.thy	Fri Jul 09 23:04:51 2010 +0100
@@ -1544,18 +1544,16 @@
 consts fa_trm :: 'a
 consts alpha_trm2 ::'a
 consts fa_trm2 :: 'a
-(*consts ast :: 'a
-consts ast' :: 'a*)
-(*
+consts ast :: 'a
+consts ast' :: 'a
 notation (latex output) 
   alpha_ty ("\<approx>ty") and
   alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
   fa_trm ("fa\<^bsub>trm\<^esub>") and
-  alpha_trm2 ("\<approx>\<^bsub>assn\<^esub>\<approx>\<^bsub>trm\<^esub>") and
-  fa_trm2 ("fa\<^bsub>assn\<^esub>fa\<^bsub>trm\<^esub>") and
+  alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
+  fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
   ast ("'(as, t')") and
   ast' ("'(as', t\<PRIME> ')")
-*)
 (*>*)
 text {*
   Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
@@ -1564,10 +1562,10 @@
 
   \begin{center}
   \begin{tabular}{@ {}c @ {}}
-%  \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
-%  {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
-%  \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
-%  {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}
+  \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
+  {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
+  \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+  {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}
   \end{tabular}
   \end{center}