diff -r 003dff7410c1 -r c92850d2d16c src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Tue Sep 02 22:20:27 2008 +0200
+++ b/src/HOL/Auth/TLS.thy	Tue Sep 02 22:37:20 2008 +0200
@@ -41,7 +41,7 @@
 
 header{*The TLS Protocol: Transport Layer Security*}
 
-theory TLS imports Public NatPair begin
+theory TLS imports Public begin
 
 constdefs
   certificate      :: "[agent,key] => msg"