diff -r 8f9d09241a68 -r b50d5d694838 src/HOL/Import/HOL/list.imp
--- a/src/HOL/Import/HOL/list.imp	Wed Sep 07 00:08:09 2011 +0200
+++ b/src/HOL/Import/HOL/list.imp	Wed Sep 07 07:59:45 2011 +0900
@@ -19,7 +19,7 @@
   "REPLICATE" > "List.replicate"
   "NULL" > "List.null"
   "NIL" > "List.list.Nil"
-  "MEM" > "List.op mem"
+  "MEM" > "HOL4Compat.list_mem"
   "MAP2" > "HOL4Compat.map2"
   "MAP" > "List.map"
   "LENGTH" > "Nat.size_class.size"
@@ -30,25 +30,25 @@
   "FOLDL" > "List.foldl"
   "FLAT" > "List.concat"
   "FILTER" > "List.filter"
-  "EXISTS" > "HOL4Compat.list_exists"
+  "EXISTS" > "List.list_ex"
   "EVERY" > "List.list_all"
   "CONS" > "List.list.Cons"
   "APPEND" > "List.append"
 
 thm_maps
-  "list_size_def" > "HOL4Compat.list_size_def"
+  "list_size_def" > "HOL4Compat.list_size_def'"
   "list_size_cong" > "HOL4Base.list.list_size_cong"
   "list_nchotomy" > "HOL4Compat.list_CASES"
-  "list_induction" > "HOL4Compat.unzip.induct"
-  "list_distinct" > "List.list.simps_1"
+  "list_induction" > "HOL4Compat.list_INDUCT"
+  "list_distinct" > "List.list.distinct_1"
   "list_case_def" > "HOL4Compat.list_case_def"
   "list_case_cong" > "HOL4Compat.list_case_cong"
   "list_case_compute" > "HOL4Base.list.list_case_compute"
-  "list_INDUCT" > "HOL4Compat.unzip.induct"
+  "list_INDUCT" > "HOL4Compat.list_INDUCT"
   "list_CASES" > "HOL4Compat.list_CASES"
   "list_Axiom_old" > "HOL4Compat.list_Axiom_old"
   "list_Axiom" > "HOL4Compat.list_Axiom"
-  "list_11" > "List.list.simps_3"
+  "list_11" > "List.list.inject"
   "ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
   "ZIP_MAP" > "HOL4Base.list.ZIP_MAP"
   "ZIP" > "HOL4Compat.ZIP"
@@ -62,11 +62,11 @@
   "REVERSE_APPEND" > "List.rev_append"
   "NULL_DEF" > "HOL4Compat.NULL_DEF"
   "NULL" > "HOL4Base.list.NULL"
-  "NOT_NIL_CONS" > "List.list.simps_1"
+  "NOT_NIL_CONS" > "List.list.distinct_1"
   "NOT_EXISTS" > "HOL4Base.list.NOT_EXISTS"
   "NOT_EVERY" > "HOL4Base.list.NOT_EVERY"
   "NOT_EQ_LIST" > "HOL4Base.list.NOT_EQ_LIST"
-  "NOT_CONS_NIL" > "List.list.simps_2"
+  "NOT_CONS_NIL" > "List.list.distinct_2"
   "MEM_ZIP" > "HOL4Base.list.MEM_ZIP"
   "MEM_MAP" > "HOL4Base.list.MEM_MAP"
   "MEM_EL" > "HOL4Base.list.MEM_EL"
@@ -102,7 +102,7 @@
   "EXISTS_MEM" > "HOL4Base.list.EXISTS_MEM"
   "EXISTS_DEF" > "HOL4Compat.list_exists_DEF"
   "EXISTS_CONG" > "HOL4Base.list.EXISTS_CONG"
-  "EXISTS_APPEND" > "HOL4Base.list.EXISTS_APPEND"
+  "EXISTS_APPEND" > "List.list_ex_append"
   "EVERY_MONOTONIC" > "HOL4Base.list.EVERY_MONOTONIC"
   "EVERY_MEM" > "HOL4Base.list.EVERY_MEM"
   "EVERY_EL" > "HOL4Base.list.EVERY_EL"
@@ -115,7 +115,7 @@
   "EL_ZIP" > "HOL4Base.list.EL_ZIP"
   "EL" > "HOL4Base.list.EL"
   "CONS_ACYCLIC" > "HOL4Base.list.CONS_ACYCLIC"
-  "CONS_11" > "List.list.simps_3"
+  "CONS_11" > "List.list.inject"
   "CONS" > "HOL4Base.list.CONS"
   "APPEND_eq_NIL" > "HOL4Base.list.APPEND_eq_NIL"
   "APPEND_NIL" > "List.append_Nil2"