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