src/HOL/Import/HOL/pair.imp
changeset 17658 ab7954ba5261
parent 17644 bd59bfd4bf37
child 17694 b7870c2bd7df
--- a/src/HOL/Import/HOL/pair.imp	Mon Sep 26 19:19:14 2005 +0200
+++ b/src/HOL/Import/HOL/pair.imp	Mon Sep 26 19:19:15 2005 +0200
@@ -21,7 +21,7 @@
   "##" > "prod_fun"
 
 thm_maps
-  "pair_induction" > "Datatype.prod.induct"
+  "pair_induction" > "Datatype.prod.induct_correctness"
   "pair_case_thm" > "Product_Type.split"
   "pair_case_def" > "HOL4Compat.pair_case_def"
   "pair_case_cong" > "HOL4Base.pair.pair_case_cong"