--- 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) =