diff -r 3a2efce3e992 -r 544cef16045b src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Mar 29 19:13:58 2008 +0100
+++ b/src/HOL/List.thy	Sat Mar 29 19:14:00 2008 +0100
@@ -591,7 +591,7 @@
 - or both lists end in the same list.
 *}
 
-ML_setup {*
+ML {*
 local
 
 fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =