# HG changeset patch
# User wenzelm
# Date 952961092 -3600
# Node ID 8f8eb220d9aafebedc236ae3b69b122d0195beb8
# Parent  0ed4b608ba4bfa95239d458da0b28d83c2bd941c
replaced exhaust_tac by case_tac;

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 = $_;