# HG changeset patch
# User haftmann
# Date 1242232896 -7200
# Node ID a9f728dc5c8ec714a4c9aa0144aa57063daf9b88
# Parent  bfafc204042a25f94ab6798a306475d9d2341d8c
dropped sort constraint on predicate equality

diff -r bfafc204042a -r a9f728dc5c8e src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed May 13 18:41:35 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed May 13 18:41:36 2009 +0200
@@ -610,7 +610,7 @@
     (simp_all add: Seq_def single_less_eq_eval contained_less_eq)
 
 lemma eq_pred_code [code]:
-  fixes P Q :: "'a::eq pred"
+  fixes P Q :: "'a pred"
   shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
   unfolding eq by auto