--- a/src/HOL/Quotient.thy Fri Nov 21 22:59:32 2014 +0100
+++ b/src/HOL/Quotient.thy Sat Nov 22 11:36:00 2014 +0100
@@ -749,10 +749,10 @@
text {* Auxiliary data for the quotient package *}
named_theorems quot_equiv "equivalence relation theorems"
-named_theorems quot_respect "respectfulness theorems"
-named_theorems quot_preserve "preservation theorems"
-named_theorems id_simps "identity simp rules for maps"
-named_theorems quot_thm "quotient theorems"
+ and quot_respect "respectfulness theorems"
+ and quot_preserve "preservation theorems"
+ and id_simps "identity simp rules for maps"
+ and quot_thm "quotient theorems"
ML_file "Tools/Quotient/quotient_info.ML"
declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]