src/HOL/Isar_Examples/Hoare.thy

--- a/src/HOL/Isar_Examples/Hoare.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -8,7 +8,6 @@
 
 theory Hoare
 imports Main
-uses ("~~/src/HOL/Hoare/hoare_tac.ML")
 begin
 
 subsection {* Abstract syntax and semantics *}
@@ -402,7 +401,7 @@
 
 lemmas AbortRule = SkipRule  -- "dummy version"
 
-use "~~/src/HOL/Hoare/hoare_tac.ML"
+ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
 
 method_setup hoare = {*
   Scan.succeed (fn ctxt =>