diff -r 6601c227c5bf -r a6eab3be095b src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Sun Apr 11 17:46:42 2010 +0200
+++ b/src/HOL/Quotient.thy	Mon Apr 12 13:19:28 2010 +0200
@@ -747,7 +747,7 @@
   about the lifted theorem in a tactic.
 *}
 definition
-  "Quot_True x \<equiv> True"
+  "Quot_True (x :: 'a) \<equiv> True"
 
 lemma
   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"