src/HOL/Import/import_syntax.ML
changeset 37165 c2e27ae53c2a
parent 36960 01594f816e3a
child 38803 38b68972721b
     1.1 --- a/src/HOL/Import/import_syntax.ML	Fri May 28 17:48:18 2010 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Fri May 28 18:15:22 2010 +0200
     1.3 @@ -39,11 +39,11 @@
     1.4                                        |> Sign.add_path thyname
     1.5                                        |> add_dump (";setup_theory " ^ thyname))
     1.6  
     1.7 -fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
     1.8 +fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I: theory -> theory)
     1.9  val skip_import_dir = Parse.string >> do_skip_import_dir
    1.10  
    1.11  val lower = String.map Char.toLower
    1.12 -fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
    1.13 +fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I: theory -> theory)
    1.14  val skip_import = Parse.short_ident >> do_skip_import
    1.15  
    1.16  fun end_import toks =