src/CTT/CTT.thy

--- a/src/CTT/CTT.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/CTT/CTT.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -7,9 +7,9 @@
 
 theory CTT
 imports Pure
-uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
 begin
 
+ML_file "~~/src/Provers/typedsimp.ML"
 setup Pure_Thy.old_appl_syntax_setup
 
 typedecl i
@@ -460,7 +460,7 @@
 fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
 *}
 
-use "rew.ML"
+ML_file "rew.ML"
 
 
 subsection {* The elimination rules for fst/snd *}