# HG changeset patch
# User haftmann
# Date 1324738389 -3600
# Node ID 2af982715e5c0f1fecb98daa0f5cdf907deff229
# Parent  7b3a18670a9ffc7063336636f6b8b5a9a474f85f
generalized type signature to permit overloading on `set`

diff -r 7b3a18670a9f -r 2af982715e5c src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Dec 24 15:53:08 2011 +0100
+++ b/src/HOL/Nat.thy	Sat Dec 24 15:53:09 2011 +0100
@@ -1200,9 +1200,9 @@
   functions and relations, in order to share the same syntax.
 *}
 
-consts compow :: "nat \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
+consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
 
-abbreviation compower :: "('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "^^" 80) where
+abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80) where
   "f ^^ n \<equiv> compow n f"
 
 notation (latex output)