src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Fri Feb 07 17:15:30 1997 +0100
+++ b/src/FOL/simpdata.ML	Mon Feb 10 12:31:54 1997 +0100
@@ -12,7 +12,7 @@
  (writeln s;  
   prove_goal IFOL.thy s
    (fn prems => [ (cut_facts_tac prems 1), 
-                  (Int.fast_tac 1) ]));
+                  (IntPr.fast_tac 1) ]));
 
 val conj_simps = map int_prove_fun
  ["P & True <-> P",      "True & P <-> P",
@@ -123,7 +123,7 @@
 
 fun int_prove nm thm  = qed_goal nm IFOL.thy thm
     (fn prems => [ (cut_facts_tac prems 1), 
-                   (Int.fast_tac 1) ]);
+                   (IntPr.fast_tac 1) ]);
 
 fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [fast_tac FOL_cs 1]);