diff -r cfe2b0803a51 -r 267f30cbe2cb src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Sep 20 13:02:30 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Sep 20 13:53:03 2006 +0200
@@ -125,8 +125,6 @@
     in
 	not (tp_level = ResHolClause.T_NONE)
     end;
-val include_combS = ResHolClause.include_combS;
-val include_min_comb = ResHolClause.include_min_comb;
 
 fun atp_input_file () =
     let val file = !problem_name