src/HOL/List.thy
changeset 51272 9c8d63b4b6be
parent 51173 3cbb4e95a565
child 51314 eac4bb5adbf9
--- a/src/HOL/List.thy	Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/List.thy	Mon Feb 25 12:17:50 2013 +0100
@@ -444,7 +444,7 @@
   in [(@{syntax_const "_listcompr"}, lc_tr)] end
 *}
 
-ML {*
+ML_val {*
   let
     val read = Syntax.read_term @{context};
     fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1);