--- a/src/HOL/Relation_Power.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Relation_Power.thy Sat Dec 01 18:52:32 2001 +0100
@@ -15,7 +15,7 @@
Relation_Power = Nat +
instance
- set :: (term) {power} (* only ('a * 'a) set should be in power! *)
+ set :: (type) power (* only ('a * 'a) set should be in power! *)
primrec (relpow)
"R^0 = Id"
@@ -23,7 +23,7 @@
instance
- fun :: (term,term)power (* only 'a => 'a should be in power! *)
+ fun :: (type, type) power (* only 'a => 'a should be in power! *)
primrec (funpow)
"f^0 = id"