diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -27,7 +27,7 @@
 
 text {* valid contexts *}
 
-inductive2
+inductive
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
 where
     v1[intro]: "valid []"
@@ -36,7 +36,7 @@
 equivariance valid
 
 text{* typing judgements *}
-inductive2
+inductive
   typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"