src/FOLP/simpdata.ML
changeset 2603 4988dda71c0b
parent 1463 49ca5e875691
child 3836 f1a1817659e6
--- a/src/FOLP/simpdata.ML	Mon Feb 10 12:34:54 1997 +0100
+++ b/src/FOLP/simpdata.ML	Mon Feb 10 12:52:11 1997 +0100
@@ -10,7 +10,7 @@
 
 fun int_prove_fun_raw s = 
     (writeln s;  prove_goal IFOLP.thy s
-       (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));
+       (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
 
 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);