--- a/src/HOL/List.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/List.thy Wed Aug 22 22:55:41 2012 +0200
@@ -6,9 +6,6 @@
theory List
imports Plain Presburger Code_Numeral Quotient ATP
-uses
- ("Tools/list_code.ML")
- ("Tools/list_to_set_comprehension.ML")
begin
datatype 'a list =
@@ -485,7 +482,7 @@
*)
-use "Tools/list_to_set_comprehension.ML"
+ML_file "Tools/list_to_set_comprehension.ML"
simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
@@ -5522,7 +5519,7 @@
subsubsection {* Pretty lists *}
-use "Tools/list_code.ML"
+ML_file "Tools/list_code.ML"
code_type list
(SML "_ list")