--- a/Quot/Examples/LamEx.thy	Sat Jan 16 03:56:00 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Sat Jan 16 04:23:27 2010 +0100
@@ -464,14 +464,6 @@
 apply(case_tac "a=b")
 apply(clarify)
 apply(simp)
-apply(subst pt_swap_bij'')
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(subst pt_swap_bij'')
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(simp)
-apply(generate_fresh "name")
 (* probably true *)
 sorry