--- a/src/HOL/Tools/res_hol_clause.ML Thu Oct 12 15:50:16 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Thu Oct 12 15:50:43 2006 +0200
@@ -23,8 +23,9 @@
val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";
-(* a flag to set if we use extra combinators B',C',S' *)
-val use_combB'C'S' = ref true;
+(*A flag to set if we use extra combinators B',C',S', currently FALSE as the 5 standard
+ combinators appear to work best.*)
+val use_combB'C'S' = ref false;
val combI_count = ref 0;
val combK_count = ref 0;