# HG changeset patch
# User wenzelm
# Date 1275063322 -7200
# Node ID c2e27ae53c2a156342ba5c89bbd40e785cfb4bd1
# Parent  8b4617ad1593402ba4a661797d06888022bb1021
made SML/NJ quite happy;

diff -r 8b4617ad1593 -r c2e27ae53c2a src/HOL/Import/import_syntax.ML
--- 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 =
diff -r 8b4617ad1593 -r c2e27ae53c2a src/HOL/Tools/SMT/smt_word.ML
--- a/src/HOL/Tools/SMT/smt_word.ML	Fri May 28 17:48:18 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_word.ML	Fri May 28 18:15:22 2010 +0200
@@ -121,7 +121,7 @@
     else NONE
 in
 
-val smtlib_builtins = {
+val smtlib_builtins : SMTLIB_Interface.builtins = {
   builtin_typ = smtlib_builtin_typ,
   builtin_num = smtlib_builtin_num,
   builtin_func = (fn (n, T) => fn ts => smtlib_builtin_func n T ts),
diff -r 8b4617ad1593 -r c2e27ae53c2a src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri May 28 17:48:18 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri May 28 18:15:22 2010 +0200
@@ -571,7 +571,7 @@
         val defs = con_betas @ sel_defs;
         val rules = abs_inv :: @{thms sel_app_rules};
         val tacs = [asm_simp_tac (simple_ss addsimps rules) 1];
-        fun sel_apps_of (i, (con, args)) =
+        fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
           let
             val Ts : typ list = map #3 args;
             val ns : string list = Datatype_Prop.make_tnames Ts;
diff -r 8b4617ad1593 -r c2e27ae53c2a src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri May 28 17:48:18 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri May 28 18:15:22 2010 +0200
@@ -452,7 +452,7 @@
 
     val decisive_lemma =
       let
-        fun iso_locale info =
+        fun iso_locale (info : iso_info) =
             @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info];
         val iso_locale_thms = map iso_locale iso_infos;
         val decisive_abs_rep_thms =