src/HOL/Tools/Lifting/lifting_def.ML
changeset 60239 755e11e2e15d
parent 60231 0daab758e087
child 60784 4f590c08fd5d
     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)