--- a/Nominal/Nominal2_Base.thy	Wed Mar 27 16:09:46 2013 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Mar 27 17:23:00 2013 +0000
@@ -3319,11 +3319,6 @@
   apply (auto simp add: fresh_Pair intro: a)
   done
 
-lemma "1 = 1 &&& 2 = 2"
-apply(tactic {* ALLGOALS (asm_full_simp_tac @{simpset}) *})
-done
-
-
 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ss => fn ctrm =>
   let
      val ctxt = Simplifier.the_context ss