# HG changeset patch
# User mengj
# Date 1137882160 -3600
# Node ID ade018a624507dcef82ab21532638fad19306759
# Parent  b6925d782fae51f626fe655aeaacf9cd98b33e2e
Ensure dereference is delayed.

diff -r b6925d782fae -r ade018a62450 src/HOL/Tools/res_atp_methods.ML
--- a/src/HOL/Tools/res_atp_methods.ML	Sat Jan 21 23:07:26 2006 +0100
+++ b/src/HOL/Tools/res_atp_methods.ML	Sat Jan 21 23:22:40 2006 +0100
@@ -35,16 +35,16 @@
 
 (* vampire and eprover tactics *)
 
-val vampire_tac = res_atp_tac vampire_oracle ResAtpSetup.Auto (!vampire_time);
-val eprover_tac = res_atp_tac eprover_oracle ResAtpSetup.Auto(!eprover_time);
+fun vampire_tac st = res_atp_tac vampire_oracle ResAtpSetup.Auto (!vampire_time) st;
+fun eprover_tac st = res_atp_tac eprover_oracle ResAtpSetup.Auto (!eprover_time) st;
 
-val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.Fol(!vampire_time);
+fun vampireF_tac st = res_atp_tac vampire_oracle ResAtpSetup.Fol (!vampire_time) st;
 
-val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.Hol (!vampire_time);
+fun vampireH_tac st = res_atp_tac vampire_oracle ResAtpSetup.Hol (!vampire_time) st;
 
-val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.Fol (!eprover_time);
+fun eproverF_tac st = res_atp_tac eprover_oracle ResAtpSetup.Fol (!eprover_time) st;
 
-val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time);
+fun eproverH_tac st = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time) st;
 
 val ResAtps_setup =
   Method.add_methods