src/HOL/List.thy

           in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
 
   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);
   in
     check "[(x,y,z). b]" "if b then [(x, y, z)] else []";