--- a/Nominal/ExLet.thy	Thu Mar 25 17:30:46 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 20:12:57 2010 +0100
@@ -1,5 +1,5 @@
 theory ExLet
-imports "Parser"
+imports "Parser" "../Attic/Prove"
 begin
 
 text {* example 3 or example 5 from Terms.thy *}
@@ -8,7 +8,6 @@
 
 ML {* val _ = recursive := false  *}
 
-
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -23,6 +22,8 @@
   "bn Lnil = {}"
 | "bn (Lcons x t l) = {atom x} \<union> (bn l)"
 
+
+
 thm trm_lts.fv
 thm trm_lts.eq_iff
 thm trm_lts.bn