diff -r 64fa844064fa -r cc9359bfacf4 CookBook/Base.thy --- a/CookBook/Base.thy Wed Mar 04 14:26:21 2009 +0000 +++ b/CookBook/Base.thy Thu Mar 05 16:46:43 2009 +0000 @@ -15,5 +15,9 @@ Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); *} +ML {* + fun warning str = str + fun tracing str = str +*} end