diff -r d72ca5742f80 -r c0eafbd55de3 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/Sequents/Sequents.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -7,7 +7,6 @@
 
 theory Sequents
 imports Pure
-uses ("prover.ML")
 begin
 
 setup Pure_Thy.old_appl_syntax_setup
@@ -142,7 +141,7 @@
 
 parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
 
-use "prover.ML"
+ML_file "prover.ML"
 
 end