# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260230421 -3600
# Node ID 018aabbffd0839d9e1b9cba62f3b2024fa726a7d
# Parent  ec37a279ca550097321560566aa928434a0fdd71
removed a fixme: map_info is now checked

diff -r ec37a279ca55 -r 018aabbffd08 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 23:45:51 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 01:00:21 2009 +0100
@@ -144,8 +144,7 @@
 
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
-
-(* FIXME: This should throw an exception: *)
+(* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 
 
@@ -161,9 +160,6 @@
 lemmas [quotient_equiv] =
   identity_equivp prod_equivp
 
-ML {* maps_lookup @{theory} "*" *}
-ML {* maps_lookup @{theory} "fun" *}
-
 
 (* definition of the quotient types *)
 (* FIXME: should be called quotient_typ.ML *)
diff -r ec37a279ca55 -r 018aabbffd08 Quot/Quotients.thy
--- a/Quot/Quotients.thy	Mon Dec 07 23:45:51 2009 +0100
+++ b/Quot/Quotients.thy	Tue Dec 08 01:00:21 2009 +0100
@@ -42,10 +42,6 @@
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
-
-
-
-
 fun
   noption_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
 where
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