# HG changeset patch
# User haftmann
# Date 1130513269 -7200
# Node ID 8bedb073e628ff32a2909c96467b3ecd58b68cc7
# Parent  3f5d0acdfdbac4f2c79400b96746ea7eb869f60f
circumvented smlnj value restriction

diff -r 3f5d0acdfdba -r 8bedb073e628 src/HOL/Tools/res_atp_setup.ML
--- a/src/HOL/Tools/res_atp_setup.ML	Fri Oct 28 17:27:04 2005 +0200
+++ b/src/HOL/Tools/res_atp_setup.ML	Fri Oct 28 17:27:49 2005 +0200
@@ -251,10 +251,9 @@
 			  else HEADGOAL (tac ctxt files tfrees))
     end;
 
-val atp_meth_f = atp_meth_g tptp_hyps tptp_cnf_clasimp;
+fun atp_meth_f tac = atp_meth_g tptp_hyps tptp_cnf_clasimp tac;
 
-val atp_meth_h = atp_meth_g tptp_hypsH tptp_cnf_clasimpH;
-
+fun atp_meth_h tac = atp_meth_g tptp_hypsH tptp_cnf_clasimpH tac;
 
 fun atp_meth_G atp_meth tac prems ctxt =
     let val _ = ResClause.init (ProofContext.theory_of ctxt)
@@ -264,9 +263,9 @@
     end;
 	
 
-val atp_meth_H = atp_meth_G atp_meth_h;
+fun atp_meth_H tac = atp_meth_G atp_meth_h tac;
 
-val atp_meth_F = atp_meth_G atp_meth_f;
+fun atp_meth_F tac = atp_meth_G atp_meth_f tac;
 
 
 val atp_method_H = Method.bang_sectioned_args rules_modifiers o atp_meth_H;