
diff -r d3fcc1a0272c -r 90bee31628dc CookBook/Base.thy
--- a/CookBook/Base.thy	Thu Feb 26 13:46:05 2009 +0100
+++ b/CookBook/Base.thy	Thu Mar 12 08:11:02 2009 +0100
@@ -14,6 +14,10 @@
     (OuterParse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
 *}
-
-
+(*
+ML {*
+  fun warning str = str
+  fun tracing str = str
+*}
+*)
 end




