1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Oct 14 15:21:45 2013 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Oct 11 18:36:51 2013 +0200
     1.3 @@ -758,7 +758,11 @@
     1.4      fun setup_typedef () = 
     1.5        case opt_reflp_xthm of
     1.6          SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
     1.7 -        | NONE => setup_by_typedef_thm gen_code input_thm lthy
     1.8 +        | NONE => (
     1.9 +          case opt_par_xthm of
    1.10 +            SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
    1.11 +            | NONE => setup_by_typedef_thm gen_code input_thm lthy
    1.12 +        )
    1.13    in
    1.14      case input_term of
    1.15        (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()