# HG changeset patch
# User wenzelm
# Date 1134485201 -3600
# Node ID fdefc3cd45c5952a8525d313e49fc0c48a33885c
# Parent  2e901da7cd3a0db895290c55dce3fb8b54385b6a
Poplog/pml provides a proper print function already!

diff -r 2e901da7cd3a -r fdefc3cd45c5 src/Pure/ML-Systems/poplogml.ML
--- a/src/Pure/ML-Systems/poplogml.ML	Tue Dec 13 15:34:21 2005 +0100
+++ b/src/Pure/ML-Systems/poplogml.ML	Tue Dec 13 15:46:41 2005 +0100
@@ -24,7 +24,6 @@
 fun print_depth _ = ();
 
 fun exception_trace f = f ();
-fun print x = x;
 fun profile (n: int) f x = f x;