src/HOL/Proofs/Extraction/Warshall.thy
changeset 51272 9c8d63b4b6be
parent 39157 b98909faaea8
child 58272 61d94335ef6c
--- 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