diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/NumberTheory/Int2.thy
--- a/src/HOL/NumberTheory/Int2.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/NumberTheory/Int2.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -8,7 +8,7 @@
 theory Int2 imports Finite2 WilsonRuss begin
 
 definition
-  MultInv :: "int => int => int"
+  MultInv :: "int => int => int" where
   "MultInv p x = x ^ nat (p - 2)"