--- a/src/Pure/Isar/isar_thy.ML Tue May 17 18:10:31 2005 +0200 +++ b/src/Pure/Isar/isar_thy.ML Tue May 17 18:10:31 2005 +0200 @@ -685,4 +685,3 @@ val context = init_context (ThyInfo.quiet_update_thy true); end; -