diff -r 054332e39e0a -r 868129805da8 src/HOL/ex/nbe.thy
--- a/src/HOL/ex/nbe.thy	Fri Mar 10 16:05:34 2006 +0100
+++ b/src/HOL/ex/nbe.thy	Fri Mar 10 16:21:49 2006 +0100
@@ -99,15 +99,15 @@
 norm_by_eval "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))"
 norm_by_eval "last[a,b,c]"
 
-text {*
+(
   won't work since it relies on 
   polymorphically used ad-hoc overloaded function:
   norm_by_eval "max 0 (0::nat)"
-*}
+*)
 
-text {*
+text (*
   Numerals still take their time\<dots>
-*}
+*)
 
 end