# HG changeset patch
# User wenzelm
# Date 924614427 -7200
# Node ID 13c779aec65a234e1525abfe3f0090f46ccdf025
# Parent  837e645e14bd2a9b975b8329aaa406920c0590c2
temporarily fake quiet_mode;

diff -r 837e645e14bd -r 13c779aec65a src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Apr 20 15:19:52 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue Apr 20 15:20:27 1999 +0200
@@ -22,8 +22,12 @@
 structure RecdefPackage: RECDEF_PACKAGE =
 struct
 
+(* FIXME tmp
 val quiet_mode = Tfl.quiet_mode;
 val message = Tfl.message;
+*)
+val quiet_mode = ref false;
+val message = writeln;