abstraction is now turned OFF...
authorpaulson
Thu Oct 12 15:50:16 2006 +0200 (2006-10-12 ago)
changeset 20996197e6875d637
parent 20995 51c41f167adc
child 20997 4b500d78cb4f
abstraction is now turned OFF...
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Oct 12 15:48:13 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 12 15:50:16 2006 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Transformation of axiom rules (elim/intro/etc) into CNF forms.
     1.5  *)
     1.6  
     1.7 -(*FIXME: does this signature serve any purpose?*)
     1.8 +(*unused during debugging*)
     1.9  signature RES_AXIOMS =
    1.10    sig
    1.11    val elimRule_tac : thm -> Tactical.tactic
    1.12 @@ -32,9 +32,11 @@
    1.13  
    1.14  struct
    1.15  
    1.16 -(*FIXME DELETE: For running the comparison between combinators and abstractions.
    1.17 -  CANNOT be a ref, as the setting is used while Isabelle is built.*)
    1.18 -val abstract_lambdas = true;
    1.19 +(*For running the comparison between combinators and abstractions.
    1.20 +  CANNOT be a ref, as the setting is used while Isabelle is built.
    1.21 +  Currently FALSE, i.e. all the "abstraction" code below is unused, but so far
    1.22 +  it seems to be inferior to combinators...*)
    1.23 +val abstract_lambdas = false;
    1.24  
    1.25  val trace_abs = ref false;
    1.26  
    1.27 @@ -509,7 +511,6 @@
    1.28            val (thy'', ths') = declare_abstract' (thy', ths)
    1.29        in  (thy'', th_defs @ ths')  end;
    1.30  
    1.31 -(*FIXME DELETE if we decide to switch to abstractions*)
    1.32  fun declare_abstract (thy, ths) =
    1.33    if abstract_lambdas then declare_abstract' (thy, ths)
    1.34    else (thy, map Drule.eta_contraction_rule ths);