# HG changeset patch
# User bulwahn
# Date 1324399221 -3600
# Node ID d7d6c8cfb6f677402b349f709d70b3d07b6d53b6
# Parent  8748456601197a4c3ad463395646a4d9ec765300
removing some debug output in quotient_definition

diff -r 874845660119 -r d7d6c8cfb6f6 src/HOL/Tools/Quotient/quotient_def.ML
--- 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'