# HG changeset patch
# User paulson
# Date 1160661016 -7200
# Node ID 197e6875d637f07818c95307d1d248e17b177285
# Parent  51c41f167adc890056b300c535d7d4e91594393c
abstraction is now turned OFF...

diff -r 51c41f167adc -r 197e6875d637 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Oct 12 15:48:13 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 12 15:50:16 2006 +0200
@@ -5,7 +5,7 @@
 Transformation of axiom rules (elim/intro/etc) into CNF forms.
 *)
 
-(*FIXME: does this signature serve any purpose?*)
+(*unused during debugging*)
 signature RES_AXIOMS =
   sig
   val elimRule_tac : thm -> Tactical.tactic
@@ -32,9 +32,11 @@
 
 struct
 
-(*FIXME DELETE: For running the comparison between combinators and abstractions.
-  CANNOT be a ref, as the setting is used while Isabelle is built.*)
-val abstract_lambdas = true;
+(*For running the comparison between combinators and abstractions.
+  CANNOT be a ref, as the setting is used while Isabelle is built.
+  Currently FALSE, i.e. all the "abstraction" code below is unused, but so far
+  it seems to be inferior to combinators...*)
+val abstract_lambdas = false;
 
 val trace_abs = ref false;
 
@@ -509,7 +511,6 @@
           val (thy'', ths') = declare_abstract' (thy', ths)
       in  (thy'', th_defs @ ths')  end;
 
-(*FIXME DELETE if we decide to switch to abstractions*)
 fun declare_abstract (thy, ths) =
   if abstract_lambdas then declare_abstract' (thy, ths)
   else (thy, map Drule.eta_contraction_rule ths);