src/HOL/SMT_Examples/boogie.ML

--- a/src/HOL/SMT_Examples/boogie.ML	Tue Mar 18 16:45:14 2014 +0100
+++ b/src/HOL/SMT_Examples/boogie.ML	Tue Mar 18 17:39:03 2014 +0100
@@ -317,7 +317,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "boogie_file"}
     "prove verification condition from .b2i file"
-    (Thy_Load.provide_parse_files "boogie_file" >> (fn files =>
+    (Resources.provide_parse_files "boogie_file" >> (fn files =>
       Toplevel.theory (fn thy =>
         let
           val ([{lines, ...}], thy') = files thy;