diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -16,7 +16,7 @@
 subsection {* Definitions and lemmas *}
 
 definition
-  inv :: "int => int => int"
+  inv :: "int => int => int" where
   "inv p a = (a^(nat (p - 2))) mod p"
 
 consts