--- a/src/HOL/Import/hol4rews.ML Wed Jan 12 15:09:26 2011 +0100
+++ b/src/HOL/Import/hol4rews.ML Wed Jan 12 15:15:51 2011 +0100
@@ -319,6 +319,7 @@
val curmaps = HOL4TypeMaps.get thy
val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
+ (* FIXME avoid handle x *)
handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
val upd_thy = HOL4TypeMaps.put newmaps thy