diff -r c33b542394f3 -r 8279a25ad0ae src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 28 18:25:23 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 28 19:16:11 2007 +0200
@@ -32,7 +32,7 @@
   fixes T::"ty"
   and   pi::"name prm"
   shows "pi\<bullet>T = T"
-  by (induct T rule: ty.induct_weak) (simp_all)
+  by (induct T rule: ty.weak_induct) (simp_all)
 
 lemma fresh_ty[simp]:
   fixes x::"name" 
@@ -43,7 +43,7 @@
 lemma ty_cases:
   fixes T::ty
   shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
-by (induct T rule:ty.induct_weak) (auto)
+by (induct T rule:ty.weak_induct) (auto)
 
 instance ty :: size ..
 
@@ -399,11 +399,11 @@
 using a
 apply(induct)
 apply(rule QAN_Reduce)
-apply(rule whr_def_eqvt)
+apply(rule whr_def.eqvt)
 apply(assumption)+
 apply(rule QAN_Normal)
 apply(auto)
-apply(drule_tac pi="rev pi" in whr_def_eqvt)
+apply(drule_tac pi="rev pi" in whr_def.eqvt)
 apply(perm_simp)
 done
 
@@ -494,7 +494,7 @@
   obtain y where fs2: "y\<sharp>(\<Gamma>,t,u)" and "(y,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^isub>2" 
     using h by auto
   then have "([(x,y)]\<bullet>((y,T\<^isub>1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) \<Leftrightarrow> [(x,y)]\<bullet> App u (Var y) : T\<^isub>2" 
-    using  alg_equiv_eqvt[simplified] by blast
+    using  alg_equiv.eqvt[simplified] by blast
   then show ?thesis using fs fs2 by (perm_simp)
 qed