# HG changeset patch
# User paulson
# Date 864998441 -7200
# Node ID 80f0d0b2f4044c499a6ef81886cc4a37f00770ef
# Parent  5c5fdce3a4e4fd5001cd04631ca74e15672bd55b
Overloading of "^" requires a type constraint

diff -r 5c5fdce3a4e4 -r 80f0d0b2f404 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Fri May 30 15:19:58 1997 +0200
+++ b/src/HOL/RelPow.ML	Fri May 30 15:20:41 1997 +0200
@@ -6,7 +6,7 @@
 
 open RelPow;
 
-goal RelPow.thy "R^1 = R";
+goal RelPow.thy "!!R:: ('a*'a)set. R^1 = R";
 by (Simp_tac 1);
 qed "rel_pow_1";
 Addsimps [rel_pow_1];