# HG changeset patch
# User haftmann
# Date 1289829561 -3600
# Node ID 9a173a22771c97940f6f86f403773220684038d5
# Parent  7850b4cc15070609bbbbeefabeac90fc90e56e52
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)

diff -r 7850b4cc1507 -r 9a173a22771c src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Mon Nov 15 14:14:38 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Mon Nov 15 14:59:21 2010 +0100
@@ -9,7 +9,7 @@
 begin
 
 fun
-  option_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
+  option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool"
 where
   "option_rel R None None = True"
 | "option_rel R (Some x) None = False"
diff -r 7850b4cc1507 -r 9a173a22771c src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Mon Nov 15 14:14:38 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Mon Nov 15 14:59:21 2010 +0100
@@ -9,7 +9,7 @@
 begin
 
 fun
-  sum_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+  sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
 where
   "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False"