src/HOL/Nominal/Examples/SN.thy

--- a/src/HOL/Nominal/Examples/SN.thy	Wed Mar 28 17:27:44 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Mar 28 18:25:23 2007 +0200
@@ -93,7 +93,7 @@
 apply(rule conjI)
 apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
 apply(force dest!: supp_beta simp add: fresh_def)
-apply(force intro!: eqvt)
+apply(force intro!: eqvts)
 done
 
 lemma beta_subst: