--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed Sep 06 16:54:12 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed Sep 06 17:17:08 2000 +0200
@@ -695,7 +695,7 @@
by (res_inst_tac [("x","schB")] spec 1);
by (res_inst_tac [("x","tr")] spec 1);
by (thin_tac' 5 1);
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
by (REPEAT (rtac allI 1));
ren "tr schB schA" 1;
by (strip_tac 1);
@@ -935,7 +935,7 @@
by (res_inst_tac [("x","schB")] spec 1);
by (res_inst_tac [("x","tr")] spec 1);
by (thin_tac' 5 1);
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
by (REPEAT (rtac allI 1));
ren "tr schB schA" 1;
by (strip_tac 1);