# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263395642 -3600
# Node ID 999870716cc8d81b06f85520566ab4c75641b6cc
# Parent  6a27fc81c42f65249bac8061498932be8f0d5833
Better error message for definition failure.

diff -r 6a27fc81c42f -r 999870716cc8 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Wed Jan 13 15:17:52 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Jan 13 16:14:02 2010 +0100
@@ -38,7 +38,9 @@
 *)
 fun quotient_def mx attr lhs rhs lthy =
 let
-  val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
+  val (lhs_str, lhs_ty) =
+    dest_Free lhs
+    handle TERM _ => error "The name for the new constant has to be a Free; check that it is not defined yet."
   val qconst_bname = Binding.name lhs_str;
   val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)