src/HOL/Proofs/Extraction/Higman_Extraction.thy

--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -88,7 +88,7 @@
   | "f2 (Suc (Suc 0)) = [B, A]"
   | "f2 _ = []"
 
-ML {*
+ML_val {*
 local
   val higman_idx = @{code higman_idx};
   val g1 = @{code g1};