diff -r 364716401696 -r 20deab90494e src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Sat Sep 03 17:32:45 2011 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Sat Sep 03 17:56:33 2011 +0200
@@ -1,7 +1,7 @@
 header {* Simply-typed lambda-calculus with let and tuple patterns *}
 
 theory Pattern
-imports Nominal
+imports "../Nominal"
 begin
 
 no_syntax
@@ -622,7 +622,7 @@
     (auto simp add: Cons_eq_append_conv fresh_star_def
      fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append
      supp_prod fresh_prod supp_atm fresh_atm
-     dest: notE [OF iffD1 [OF fresh_def [THEN meta_eq_to_obj_eq]]])
+     dest: notE [OF iffD1 [OF fresh_def]])
 
 lemma perm_mem_left: "(x::name) \<in> ((pi::name prm) \<bullet> A) \<Longrightarrow> (rev pi \<bullet> x) \<in> A"
   by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp)