Extended combinators now disabled
authorpaulson
Thu Oct 12 15:50:43 2006 +0200 (2006-10-12)
changeset 209974b500d78cb4f
parent 20996 197e6875d637
child 20998 714a08286899
Extended combinators now disabled
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Oct 12 15:50:16 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Oct 12 15:50:43 2006 +0200
     1.3 @@ -23,8 +23,9 @@
     1.4  val equal_imp_fequal = thm "Reconstruction.equal_imp_fequal";
     1.5  
     1.6  
     1.7 -(* a flag to set if we use extra combinators B',C',S' *)
     1.8 -val use_combB'C'S' = ref true;
     1.9 +(*A flag to set if we use extra combinators B',C',S', currently FALSE as the 5 standard
    1.10 +  combinators appear to work best.*)
    1.11 +val use_combB'C'S' = ref false;
    1.12  
    1.13  val combI_count = ref 0;
    1.14  val combK_count = ref 0;