equal
deleted
inserted
replaced
415 end; |
415 end; |
416 |
416 |
417 fun add_hol4_type_mapping bthy bconst internal isaconst thy = |
417 fun add_hol4_type_mapping bthy bconst internal isaconst thy = |
418 let |
418 let |
419 val curmaps = HOL4TypeMaps.get thy |
419 val curmaps = HOL4TypeMaps.get thy |
420 val _ = message ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) |
420 val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else "")) |
421 val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst)),curmaps) |
421 val newmaps = StringPair.update_new(((bthy,bconst),(internal,isaconst)),curmaps) |
422 val upd_thy = HOL4TypeMaps.put newmaps thy |
422 handle x => let val (internal, isaconst') = the (StringPair.lookup (curmaps, (bthy, bconst))) in |
|
423 warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end |
|
424 val upd_thy = HOL4TypeMaps.put newmaps thy |
423 in |
425 in |
424 upd_thy |
426 upd_thy |
425 end; |
427 end; |
426 |
428 |
427 fun add_hol4_pending bthy bthm hth thy = |
429 fun add_hol4_pending bthy bthm hth thy = |