# HG changeset patch
# User wenzelm
# Date 1430656548 -7200
# Node ID 755e11e2e15d2704aba6c7bde3afd155eaa1df0b
# Parent  52d02564242a055c06233d5e373c01135d18f722
make SML/NJ more happy;

diff -r 52d02564242a -r 755e11e2e15d src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Sun May 03 14:12:10 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun May 03 14:35:48 2015 +0200
@@ -565,7 +565,7 @@
   par_thms - a parametricity theorem for rhs
 *)
 
-fun add_lift_def config var qty rhs rsp_thm par_thms lthy =
+fun add_lift_def (config: config) var qty rhs rsp_thm par_thms lthy =
   let
     val rty = fastype_of rhs
     val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
diff -r 52d02564242a -r 755e11e2e15d src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun May 03 14:12:10 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun May 03 14:35:48 2015 +0200
@@ -589,8 +589,8 @@
 
 (** from parsed parameters to the config record **)
 
-fun map_config_code_dt f1 f2 { code_dt = code_dt, lift_config = lift_config } =
-  { code_dt = f1 code_dt, lift_config = f2 lift_config }
+fun map_config_code_dt f1 f2 ({code_dt = code_dt, lift_config = lift_config}: config_code_dt) =
+  {code_dt = f1 code_dt, lift_config = f2 lift_config}
 
 fun update_config_code_dt nval = map_config_code_dt (K nval) I
 
diff -r 52d02564242a -r 755e11e2e15d src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 03 14:12:10 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 03 14:35:48 2015 +0200
@@ -37,7 +37,7 @@
 type config = { notes: bool };
 val default_config = { notes = true };
 
-fun define_crel config rep_fun lthy =
+fun define_crel (config: config) rep_fun lthy =
   let
     val (qty, rty) = (dest_funT o fastype_of) rep_fun
     val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
@@ -63,7 +63,7 @@
     warning warning_msg
   end
 
-fun define_pcrel config crel lthy =
+fun define_pcrel (config: config) crel lthy =
   let
     val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy
     val [rty', qty] = (binder_types o fastype_of) fixed_crel
@@ -122,10 +122,12 @@
       error error_msg
     end
 in
-  fun define_pcr_cr_eq config lthy pcr_rel_def =
+  fun define_pcr_cr_eq (config: config) lthy pcr_rel_def =
     let
       val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def
-      val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type o List.last o binder_types o fastype_of) lhs
+      val qty_name =
+        (Binding.name o Long_Name.base_name o fst o dest_Type o
+          List.last o binder_types o fastype_of) lhs
       val args = (snd o strip_comb) lhs
       
       fun make_inst var ctxt = 
@@ -519,7 +521,7 @@
   opt_par_thm - a parametricity theorem for R
 *)
 
-fun setup_by_quotient config quot_thm opt_reflp_thm opt_par_thm lthy =
+fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy =
   let
     (**)
     val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
diff -r 52d02564242a -r 755e11e2e15d src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Sun May 03 14:12:10 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Sun May 03 14:35:48 2015 +0200
@@ -73,7 +73,7 @@
        Pretty.str "don't match."])
   end
 
-fun get_quot_data quotients s =
+fun get_quot_data (quotients: quotients) s =
   case Symtab.lookup quotients s of
     SOME qdata => qdata
   | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
@@ -237,7 +237,7 @@
 type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
   comp_lift: typ -> thm * 'a -> thm * 'a }
 
-fun prove_schematic_quot_thm actions quotients ctxt (rty, qty) fold_val =
+fun prove_schematic_quot_thm (actions: 'a fold_quot_thm) quotients ctxt (rty, qty) fold_val =
   let
     fun lifting_step (rty, qty) =
       let