diff -r 340586b2305c -r 749b6870b1a1 src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Thu May 31 14:34:09 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Thu May 31 14:47:20 2007 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory Class
-imports "Nominal" 
+imports "../Nominal" 
 begin
 
 section {* Term-Calculus from Urban's PhD *}
@@ -4084,7 +4084,7 @@
   assumes a: "[a].M = [b].N" "c\<sharp>(a,b,M,N)"
   shows "M = [(a,c)]\<bullet>[(b,c)]\<bullet>N"
 using a
-apply(auto simp add: alpha' fresh_prod fresh_atm)
+apply(auto simp add: alpha_fresh fresh_prod fresh_atm)
 apply(drule sym)
 apply(perm_simp)
 done 
@@ -4095,7 +4095,7 @@
   assumes a: "[x].M = [y].N" "z\<sharp>(x,y,M,N)"
   shows "M = [(x,z)]\<bullet>[(y,z)]\<bullet>N"
 using a
-apply(auto simp add: alpha' fresh_prod fresh_atm)
+apply(auto simp add: alpha_fresh fresh_prod fresh_atm)
 apply(drule sym)
 apply(perm_simp)
 done 
@@ -4107,7 +4107,8 @@
   assumes a: "[x].[b].M = [y].[c].N" "z\<sharp>(x,y,M,N)" "a\<sharp>(b,c,M,N)"
   shows "M = [(x,z)]\<bullet>[(b,a)]\<bullet>[(c,a)]\<bullet>[(y,z)]\<bullet>N"
 using a
-apply(auto simp add: alpha' fresh_prod fresh_atm abs_supp fin_supp abs_fresh abs_perm fresh_left calc_atm)
+apply(auto simp add: alpha_fresh fresh_prod fresh_atm 
+                     abs_supp fin_supp abs_fresh abs_perm fresh_left calc_atm)
 apply(drule sym)
 apply(simp)
 apply(perm_simp)