1.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Wed Jul 20 08:46:17 2011 +0200
     1.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Wed Jul 20 10:11:08 2011 +0200
     1.3 @@ -1273,9 +1273,9 @@
     1.4    "NSUM_ADD_GEN" > "HOLLight.hollight.NSUM_ADD_GEN"
     1.5    "NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
     1.6    "NSUM_0" > "HOLLight.hollight.NSUM_0"
     1.7 -  "NOT_UNIV_PSUBSET" > "Complete_Lattice.complete_lattice_class.not_top_less"
     1.8 +  "NOT_UNIV_PSUBSET" > "Orderings.top_class.not_top_less"
     1.9    "NOT_SUC" > "Nat.Suc_not_Zero"
    1.10 -  "NOT_PSUBSET_EMPTY" > "Complete_Lattice.complete_lattice_class.not_less_bot"
    1.11 +  "NOT_PSUBSET_EMPTY" > "Orderings.bot_class.not_less_bot"
    1.12    "NOT_ODD" > "HOLLight.hollight.NOT_ODD"
    1.13    "NOT_LT" > "Orderings.linorder_class.not_less"
    1.14    "NOT_LE" > "Orderings.linorder_class.not_le"
    1.15 @@ -1644,7 +1644,7 @@
    1.16    "IMAGE_INJECTIVE_IMAGE_OF_SUBSET" > "HOLLight.hollight.IMAGE_INJECTIVE_IMAGE_OF_SUBSET"
    1.17    "IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
    1.18    "IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
    1.19 -  "IMAGE_ID" > "Fun.image_ident"
    1.20 +  "IMAGE_ID" > "Set.image_ident"
    1.21    "IMAGE_I" > "Fun.image_id"
    1.22    "IMAGE_EQ_EMPTY" > "Set.image_is_empty"
    1.23    "IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"