# HG changeset patch
# User kuncar
# Date 1392419477 -3600
# Node ID 6380313b8ed5de249511d1da8e26f46adcd161e6
# Parent  8609527278f20dd10eae83538a4481dc3a9afb31
abstract type must be a type constructor; check it

diff -r 8609527278f2 -r 6380313b8ed5 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Feb 14 18:42:43 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Feb 15 00:11:17 2014 +0100
@@ -745,25 +745,34 @@
           Const (@{const_name reflp}, _) $ _ => ()
           | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
       end
+      
+    fun check_qty qty = if not (is_Type qty) 
+          then error "The abstract type must be a type constructor."
+          else ()
 
     fun setup_quotient () = 
       let
         val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm
         val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else ()
         val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
+        val _ = check_qty (snd (quot_thm_rty_qty input_thm))
       in
         setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy
       end
-      
 
     fun setup_typedef () = 
-      case opt_reflp_xthm of
-        SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
-        | 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
-        )
+      let
+        val qty = (range_type o fastype_of o hd o get_args 2) input_term
+        val _ = check_qty qty
+      in
+        case opt_reflp_xthm of
+          SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
+          | 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
+          )
+      end
   in
     case input_term of
       (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()