diff -r 0ed4b608ba4b -r 8f8eb220d9aa lib/scripts/fixdatatype.pl
--- a/lib/scripts/fixdatatype.pl	Mon Mar 13 16:24:23 2000 +0100
+++ b/lib/scripts/fixdatatype.pl	Mon Mar 13 16:24:52 2000 +0100
@@ -23,8 +23,8 @@
     ## replace specific induct_tac by generic induct_tac
     s/[\w\.]+\.induct_tac/induct_tac/sg;
 
-    ## replace res_inst_tac ... natE by exhaust_tac
-    s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/exhaust_tac $1/sg;
+    ## replace res_inst_tac ... natE by case_tac
+    s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/case_tac $1/sg;
 
     $result = $_;