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