src/HOL/Quickcheck_Examples/Hotel_Example.thy
changeset 51272 9c8d63b4b6be
parent 51143 0a2371e7ced3
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon Feb 25 12:17:11 2013 +0100
     1.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon Feb 25 12:17:50 2013 +0100
     1.3 @@ -92,7 +92,7 @@
     1.4  setup {*  Predicate_Compile_Data.ignore_consts [@{const_name Set.member},
     1.5    @{const_name "issued"}, @{const_name "cards"}, @{const_name "isin"},
     1.6    @{const_name Collect}, @{const_name insert}] *}
     1.7 -ML {* Core_Data.force_modes_and_compilations *}
     1.8 +ML_val {* Core_Data.force_modes_and_compilations *}
     1.9  
    1.10  fun find_first :: "('a => 'b option) => 'a list => 'b option"
    1.11  where