diff -r bb276771d85c -r 94d6d29459c9 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Wed Dec 09 22:43:11 2009 +0100
+++ b/Quot/quotient_info.ML	Wed Dec 09 23:32:16 2009 +0100
@@ -65,10 +65,8 @@
   val mapname = Sign.intern_const thy mapstr
   val relname = Sign.intern_const thy relstr
 
-  (* FIXME: if you don't handle the error you also get an error with a similar message: No such constant: "bla" *)
-  fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
-        handle _ => error ("Constant " ^ s ^ " not declared.")
-  val _ =  map check [mapname, relname]
+  fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
+  val _ =  map sanity_check [mapname, relname]
 in
   maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
 end