diff -r e8d2ecf6aaac -r 9c8d63b4b6be src/HOL/Proofs/Extraction/Warshall.thy
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -256,6 +256,6 @@
   @{thm [display] warshall_correctness [no_vars]}
 *}
 
-ML "@{code warshall}"
+ML_val "@{code warshall}"
 
 end