--- a/src/HOL/RelPow.thy Tue May 09 14:16:32 2000 +0200
+++ b/src/HOL/RelPow.thy Tue May 09 14:33:43 2000 +0200
@@ -11,7 +11,7 @@
instance
set :: (term) {power} (* only ('a * 'a) set should be in power! *)
-primrec
+primrec (relpow)
"R^0 = Id"
"R^(Suc n) = R O (R^n)"