diff -r ec37a279ca55 -r 018aabbffd08 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Mon Dec 07 23:45:51 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 08 01:00:21 2009 +0100
@@ -62,6 +62,10 @@
   val tyname = Sign.intern_type thy tystr
   val mapname = Sign.intern_const thy mapstr
   val relname = Sign.intern_const thy relstr
+
+  fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
+        handle _ => error ("Constant " ^ s ^ " not declared.")
+  val _ =  map check [mapname, relname]
 in
   maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
 end