src/HOL/Library/Predicate_Compile_Quickcheck.thy
changeset 48891 c0eafbd55de3
parent 45450 dc2236b19a3d
child 51143 0a2371e7ced3
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -4,9 +4,10 @@
 
 theory Predicate_Compile_Quickcheck
 imports Main Predicate_Compile_Alternative_Defs
-uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
 begin
 
+ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
+
 setup {* Predicate_Compile_Quickcheck.setup *}
 
 end
\ No newline at end of file