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)