# HG changeset patch
# User blanchet
# Date 1286273097 -7200
# Node ID 132b799856607021d235922ee34fad7f23487be2
# Parent  cb9cac7eba29e49f3a1d5809522b3e7d7cb75293
remove needless Metis facts

diff -r cb9cac7eba29 -r 132b79985660 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Oct 05 12:04:49 2010 +0200
+++ b/src/HOL/Quotient.thy	Tue Oct 05 12:04:57 2010 +0200
@@ -319,12 +319,12 @@
 lemma ball_reg_right:
   assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
   shows "All P \<longrightarrow> Ball R Q"
-  using a by (metis COMBC_def Collect_def Collect_mem_eq)
+  using a by (metis Collect_def Collect_mem_eq)
 
 lemma bex_reg_left:
   assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
   shows "Bex R Q \<longrightarrow> Ex P"
-  using a by (metis COMBC_def Collect_def Collect_mem_eq)
+  using a by (metis Collect_def Collect_mem_eq)
 
 lemma ball_reg_left:
   assumes a: "equivp R"
@@ -381,13 +381,13 @@
   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   and     b: "Ball R P"
   shows "Ball R Q"
-  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
+  using a b by (metis Collect_def Collect_mem_eq)
 
 lemma bex_reg:
   assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   and     b: "Bex R P"
   shows "Bex R Q"
-  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
+  using a b by (metis Collect_def Collect_mem_eq)
 
 
 lemma ball_all_comm: