# HG changeset patch
# User wenzelm
# Date 1030438982 -7200
# Node ID 079af5c90d1cefe5d447dfaa49341d62ff59cae4
# Parent  934fffeb6f386b55504000fb4ca4946296ffe887
avoid duplicate fact bindings;

diff -r 934fffeb6f38 -r 079af5c90d1c src/HOL/Auth/Guard/Guard_Shared.thy
--- a/src/HOL/Auth/Guard/Guard_Shared.thy	Tue Aug 27 10:59:21 2002 +0200
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Tue Aug 27 11:03:02 2002 +0200
@@ -99,7 +99,7 @@
 lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guard n Ks"
 by (rule Guard_Nonce, simp)
 
-lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guardK n Ks"
+lemma guardK_ciph [simp]: "shrK A:Ks ==> Ciph A X:guardK n Ks"
 by (rule Guard_Key, simp)
 
 lemma Guard_init [iff]: "Guard n Ks (initState B)"