# 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