# HG changeset patch
# User wenzelm
# Date 1425498620 -3600
# Node ID 68a770a8a09fd2d61c903731b4f72e9517b98117
# Parent  4517e9a96aceccacd6f9dad6238219b8328905e7
tuned;

diff -r 4517e9a96ace -r 68a770a8a09f src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Mar 04 20:47:29 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Mar 04 20:50:20 2015 +0100
@@ -143,7 +143,7 @@
 *)
 
 fun reflp_get ctxt =
-  map_filter (fn th => if Thm.prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
+  map_filter (fn th => if Thm.no_prems th then SOME (OF1 @{thm equivp_reflp} th) else NONE
     handle THM _ => NONE) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
 
 val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}