diff -r 4a7a07c01857 -r efa24d31e595 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 13 10:34:48 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 13 11:34:05 2014 +0100
@@ -200,10 +200,10 @@
 (** invocation of Haskell interpreter **)
 
 val narrowing_engine =
-  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
+  File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
 
 val pnf_narrowing_engine =
-  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
+  File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
 
 fun exec verbose code =
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)