--- a/src/HOL/Import/import_syntax.ML Fri May 28 17:48:18 2010 +0200
+++ b/src/HOL/Import/import_syntax.ML Fri May 28 18:15:22 2010 +0200
@@ -39,11 +39,11 @@
|> Sign.add_path thyname
|> add_dump (";setup_theory " ^ thyname))
-fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
+fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I: theory -> theory)
val skip_import_dir = Parse.string >> do_skip_import_dir
val lower = String.map Char.toLower
-fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
+fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I: theory -> theory)
val skip_import = Parse.short_ident >> do_skip_import
fun end_import toks =