# HG changeset patch
# User wenzelm
# Date 1294408695 -3600
# Node ID 6e93dfec9e76af79e0099c4b93b29486a4f85ec9
# Parent  4cfb51a5a444ea1084f03694278810d520b55664
comments;

diff -r 4cfb51a5a444 -r 6e93dfec9e76 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 14:36:41 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 14:58:15 2011 +0100
@@ -10,7 +10,7 @@
 
   type maps_info = {mapfun: string, relmap: string}
   val maps_defined: theory -> string -> bool
-  (* FIXME functions called "lookup" must return option, not raise exception *)
+  (* 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
@@ -48,7 +48,7 @@
 structure Quotient_Info: QUOTIENT_INFO =
 struct
 
-exception NotFound
+exception NotFound  (* FIXME odd OCaml-ism!? *)
 
 
 (** data containers **)
diff -r 4cfb51a5a444 -r 6e93dfec9e76 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jan 07 14:36:41 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jan 07 14:58:15 2011 +0100
@@ -43,7 +43,7 @@
 
 fun atomize_thm thm =
 let
-  val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
+  val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
   val thm'' = Object_Logic.atomize (cprop_of thm')
 in
   @{thm equal_elim_rule1} OF [thm'', thm']