--- a/src/HOL/HOLCF/Fixrec.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy Wed Aug 22 22:55:41 2012 +0200
@@ -7,9 +7,6 @@
theory Fixrec
imports Plain_HOLCF
keywords "fixrec" :: thy_decl
-uses
- ("Tools/holcf_library.ML")
- ("Tools/fixrec.ML")
begin
subsection {* Pattern-match monad *}
@@ -227,8 +224,8 @@
subsection {* Initializing the fixrec package *}
-use "Tools/holcf_library.ML"
-use "Tools/fixrec.ML"
+ML_file "Tools/holcf_library.ML"
+ML_file "Tools/fixrec.ML"
method_setup fixrec_simp = {*
Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)