--- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Jun 28 07:38:39 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Jun 28 09:48:36 2010 +0200
@@ -49,7 +49,8 @@
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 is_Const rhs then () else error "The definiens should be a constant"
+ val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+ val _ = if is_Const rhs then () else warning "The definiens is not a constant"
fun sanity_test NONE _ = true
| sanity_test (SOME bind) str =