src/HOL/Tools/Lifting/lifting_setup.ML
changeset 60239 755e11e2e15d
parent 60231 0daab758e087
child 60784 4f590c08fd5d
     1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 03 14:12:10 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 03 14:35:48 2015 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  type config = { notes: bool };
     1.5  val default_config = { notes = true };
     1.6  
     1.7 -fun define_crel config rep_fun lthy =
     1.8 +fun define_crel (config: config) rep_fun lthy =
     1.9    let
    1.10      val (qty, rty) = (dest_funT o fastype_of) rep_fun
    1.11      val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
    1.12 @@ -63,7 +63,7 @@
    1.13      warning warning_msg
    1.14    end
    1.15  
    1.16 -fun define_pcrel config crel lthy =
    1.17 +fun define_pcrel (config: config) crel lthy =
    1.18    let
    1.19      val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy
    1.20      val [rty', qty] = (binder_types o fastype_of) fixed_crel
    1.21 @@ -122,10 +122,12 @@
    1.22        error error_msg
    1.23      end
    1.24  in
    1.25 -  fun define_pcr_cr_eq config lthy pcr_rel_def =
    1.26 +  fun define_pcr_cr_eq (config: config) lthy pcr_rel_def =
    1.27      let
    1.28        val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def
    1.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
    1.30 +      val qty_name =
    1.31 +        (Binding.name o Long_Name.base_name o fst o dest_Type o
    1.32 +          List.last o binder_types o fastype_of) lhs
    1.33        val args = (snd o strip_comb) lhs
    1.34        
    1.35        fun make_inst var ctxt = 
    1.36 @@ -519,7 +521,7 @@
    1.37    opt_par_thm - a parametricity theorem for R
    1.38  *)
    1.39  
    1.40 -fun setup_by_quotient config quot_thm opt_reflp_thm opt_par_thm lthy =
    1.41 +fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy =
    1.42    let
    1.43      (**)
    1.44      val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm