--- a/Quot/Examples/LamEx.thy	Thu Jan 14 19:03:08 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 23:17:21 2010 +0100
@@ -360,18 +360,11 @@
 qed
 
 
-lemma var_supp:
-  shows "supp (Var a) = ((supp a)::name set)"
-  apply(simp add: supp_def)
-  apply(simp add: pi_var2)
-  apply(simp add: var_inject)
-  done
-
 lemma var_fresh:
   fixes a::"name"
   shows "(a \<sharp> (Var b)) = (a \<sharp> b)"
   apply(simp add: fresh_def)
-  apply(simp add: var_supp)
+  apply(simp add: var_supp1)
   done
 
 end