src/HOL/Nominal/Examples/Weakening.thy
changeset 18653 7a00c80400b1
parent 18354 715d6df89fcc
child 18654 94782c7c4247
--- a/src/HOL/Nominal/Examples/Weakening.thy	Wed Jan 11 12:21:01 2006 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Wed Jan 11 14:00:11 2006 +0100
@@ -42,7 +42,7 @@
   shows   "valid (pi\<bullet>\<Gamma>)"
 using a
 apply(induct)
-apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
+apply(auto simp add: fresh_eqvt)
 done
 
 (* typing judgements *)