diff -r c55f5631a4ec -r 3ccb92dfb5e9 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 28 01:29:43 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 28 01:55:18 2007 +0200
@@ -261,7 +261,7 @@
   v_nil[intro]:  "valid []"
 | v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,T)#\<Gamma>)"
 
-nominal_inductive valid .
+equivariance valid 
 
 inductive_cases2  
   valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
@@ -562,7 +562,6 @@
   with ih have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by simp
   then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
 next
-  (* HERE *)
   case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u)
   have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T\<^isub>2" by fact
   then obtain r T\<^isub>1' v where ha: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^isub>1'\<rightarrow>T\<^isub>2" and hb: "\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^isub>1'" and eq: "u = App r v"