text delimiter fixed

--- a/src/HOL/ex/nbe.thy	Fri Mar 10 17:24:16 2006 +0100
+++ b/src/HOL/ex/nbe.thy	Fri Mar 10 17:53:53 2006 +0100
@@ -105,8 +105,8 @@
   norm_by_eval "max 0 (0::nat)"
 *)
 
-text (*
+text {*
   Numerals still take their time\<dots>
-*)
+*}
 
 end