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 =

     2.1 --- a/src/HOL/Tools/SMT/smt_word.ML	Fri May 28 17:48:18 2010 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_word.ML	Fri May 28 18:15:22 2010 +0200
     2.3 @@ -121,7 +121,7 @@
     2.4      else NONE
     2.5  in
     2.6  
     2.7 -val smtlib_builtins = {
     2.8 +val smtlib_builtins : SMTLIB_Interface.builtins = {
     2.9    builtin_typ = smtlib_builtin_typ,
    2.10    builtin_num = smtlib_builtin_num,
    2.11    builtin_func = (fn (n, T) => fn ts => smtlib_builtin_func n T ts),

     3.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri May 28 17:48:18 2010 +0200
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri May 28 18:15:22 2010 +0200
     3.3 @@ -571,7 +571,7 @@
     3.4          val defs = con_betas @ sel_defs;
     3.5          val rules = abs_inv :: @{thms sel_app_rules};
     3.6          val tacs = [asm_simp_tac (simple_ss addsimps rules) 1];
     3.7 -        fun sel_apps_of (i, (con, args)) =
     3.8 +        fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
     3.9            let
    3.10              val Ts : typ list = map #3 args;
    3.11              val ns : string list = Datatype_Prop.make_tnames Ts;

     4.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri May 28 17:48:18 2010 +0200
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri May 28 18:15:22 2010 +0200
     4.3 @@ -452,7 +452,7 @@
     4.4  
     4.5      val decisive_lemma =
     4.6        let
     4.7 -        fun iso_locale info =
     4.8 +        fun iso_locale (info : iso_info) =
     4.9              @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info];
    4.10          val iso_locale_thms = map iso_locale iso_infos;
    4.11          val decisive_abs_rep_thms =