# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1277703171 -7200
# Node ID 21ab339715cd800b1dd969a2bb1894c90c9119a8
# Parent  19fca77829eac43fc82782621bb1422604d6c806
Restrict quotient definitions to constants

diff -r 19fca77829ea -r 21ab339715cd src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sun Jun 27 08:33:01 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jun 28 07:32:51 2010 +0200
@@ -49,7 +49,7 @@
 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
 let
   val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
-  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+  val _ = if is_Const rhs then () else error "The definiens should be a constant"
   
   fun sanity_test NONE _ = true
     | sanity_test (SOME bind) str =