--- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Dec 20 17:40:18 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Dec 20 17:40:21 2011 +0100
@@ -89,7 +89,7 @@
Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
fun read_term' cnstr ctxt =
- check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
+ check_term' cnstr ctxt o Syntax.parse_term ctxt
val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'