# HG changeset patch
# User kuncar
# Date 1381509411 -7200
# Node ID ce028cf2e58e9562c17ccc200a18c70e4212e95e
# Parent  a38160ad741c23295804b7dcfaab30176b2bb33a
don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.

diff -r a38160ad741c -r ce028cf2e58e src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Oct 14 15:21:45 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Oct 11 18:36:51 2013 +0200
@@ -758,7 +758,11 @@
     fun setup_typedef () = 
       case opt_reflp_xthm of
         SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
-        | NONE => setup_by_typedef_thm gen_code input_thm lthy
+        | NONE => (
+          case opt_par_xthm of
+            SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
+            | NONE => setup_by_typedef_thm gen_code input_thm lthy
+        )
   in
     case input_term of
       (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()