make SML/NJ more happy;
authorwenzelm
Sun May 03 14:35:48 2015 +0200 (2015-05-03)
changeset 60239755e11e2e15d
parent 60238 52d02564242a
child 60240 3f61058a2de6
make SML/NJ more happy;
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Sun May 03 14:12:10 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun May 03 14:35:48 2015 +0200
     1.3 @@ -565,7 +565,7 @@
     1.4    par_thms - a parametricity theorem for rhs
     1.5  *)
     1.6  
     1.7 -fun add_lift_def config var qty rhs rsp_thm par_thms lthy =
     1.8 +fun add_lift_def (config: config) var qty rhs rsp_thm par_thms lthy =
     1.9    let
    1.10      val rty = fastype_of rhs
    1.11      val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun May 03 14:12:10 2015 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sun May 03 14:35:48 2015 +0200
     2.3 @@ -589,8 +589,8 @@
     2.4  
     2.5  (** from parsed parameters to the config record **)
     2.6  
     2.7 -fun map_config_code_dt f1 f2 { code_dt = code_dt, lift_config = lift_config } =
     2.8 -  { code_dt = f1 code_dt, lift_config = f2 lift_config }
     2.9 +fun map_config_code_dt f1 f2 ({code_dt = code_dt, lift_config = lift_config}: config_code_dt) =
    2.10 +  {code_dt = f1 code_dt, lift_config = f2 lift_config}
    2.11  
    2.12  fun update_config_code_dt nval = map_config_code_dt (K nval) I
    2.13  
     3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 03 14:12:10 2015 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 03 14:35:48 2015 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4  type config = { notes: bool };
     3.5  val default_config = { notes = true };
     3.6  
     3.7 -fun define_crel config rep_fun lthy =
     3.8 +fun define_crel (config: config) rep_fun lthy =
     3.9    let
    3.10      val (qty, rty) = (dest_funT o fastype_of) rep_fun
    3.11      val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
    3.12 @@ -63,7 +63,7 @@
    3.13      warning warning_msg
    3.14    end
    3.15  
    3.16 -fun define_pcrel config crel lthy =
    3.17 +fun define_pcrel (config: config) crel lthy =
    3.18    let
    3.19      val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy
    3.20      val [rty', qty] = (binder_types o fastype_of) fixed_crel
    3.21 @@ -122,10 +122,12 @@
    3.22        error error_msg
    3.23      end
    3.24  in
    3.25 -  fun define_pcr_cr_eq config lthy pcr_rel_def =
    3.26 +  fun define_pcr_cr_eq (config: config) lthy pcr_rel_def =
    3.27      let
    3.28        val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def
    3.29 -      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
    3.30 +      val qty_name =
    3.31 +        (Binding.name o Long_Name.base_name o fst o dest_Type o
    3.32 +          List.last o binder_types o fastype_of) lhs
    3.33        val args = (snd o strip_comb) lhs
    3.34        
    3.35        fun make_inst var ctxt = 
    3.36 @@ -519,7 +521,7 @@
    3.37    opt_par_thm - a parametricity theorem for R
    3.38  *)
    3.39  
    3.40 -fun setup_by_quotient config quot_thm opt_reflp_thm opt_par_thm lthy =
    3.41 +fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy =
    3.42    let
    3.43      (**)
    3.44      val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
     4.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Sun May 03 14:12:10 2015 +0200
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Sun May 03 14:35:48 2015 +0200
     4.3 @@ -73,7 +73,7 @@
     4.4         Pretty.str "don't match."])
     4.5    end
     4.6  
     4.7 -fun get_quot_data quotients s =
     4.8 +fun get_quot_data (quotients: quotients) s =
     4.9    case Symtab.lookup quotients s of
    4.10      SOME qdata => qdata
    4.11    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    4.12 @@ -237,7 +237,7 @@
    4.13  type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
    4.14    comp_lift: typ -> thm * 'a -> thm * 'a }
    4.15  
    4.16 -fun prove_schematic_quot_thm actions quotients ctxt (rty, qty) fold_val =
    4.17 +fun prove_schematic_quot_thm (actions: 'a fold_quot_thm) quotients ctxt (rty, qty) fold_val =
    4.18    let
    4.19      fun lifting_step (rty, qty) =
    4.20        let