1.1 --- a/src/HOL/Nominal/Nominal.thy	Tue Sep 11 14:26:49 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 13 18:06:50 2007 +0200
     1.3 @@ -3233,6 +3233,7 @@
     1.4    (* connectives *)
     1.5    if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 
     1.6    true_eqvt false_eqvt
     1.7 +  imp_eqvt [folded induct_implies_def]
     1.8    
     1.9    (* datatypes *)
    1.10    perm_unit.simps