--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Oct 28 22:04:00 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Oct 28 22:11:06 2010 +0200
@@ -6,10 +6,11 @@
signature QUOTIENT_INFO =
sig
- exception NotFound
+ exception NotFound (* FIXME complicates signatures unnecessarily *)
type maps_info = {mapfun: string, relmap: string}
val maps_defined: theory -> string -> bool
+ (* FIXME functions called "lookup" must return option, not raise exception *)
val maps_lookup: theory -> string -> maps_info (* raises NotFound *)
val maps_update_thy: string -> maps_info -> theory -> theory
val maps_update: string -> maps_info -> Proof.context -> Proof.context