# HG changeset patch
# User paulson
# Date 1160661043 -7200
# Node ID 4b500d78cb4f24207615ec9b4a3fb08c87f2d730
# Parent  197e6875d637f07818c95307d1d248e17b177285
Extended combinators now disabled

diff -r 197e6875d637 -r 4b500d78cb4f src/HOL/Tools/res_hol_clause.ML
--- 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;