# HG changeset patch
# User urbanc
# Date 1136984411 -3600
# Node ID 7a00c80400b16ceeb511475c0af6e0cc534eaaa1
# Parent  3930a060d71b9a80a702d5a6ef0068729aaca1df
tuned the eqvt-proof

diff -r 3930a060d71b -r 7a00c80400b1 src/HOL/Nominal/Examples/Weakening.thy
--- 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 *)