src/HOL/Tools/Metis/metis_tactics.ML
changeset 42616 92715b528e78
parent 42552 e155be7125ba
child 42650 552eae49f97d
     1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon May 02 13:29:47 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon May 02 16:33:21 2011 +0200
     1.3 @@ -25,9 +25,8 @@
     1.4  open Metis_Translate
     1.5  open Metis_Reconstruct
     1.6  
     1.7 -val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
     1.8 -val (new_skolemizer, new_skolemizer_setup) =
     1.9 -  Attrib.config_bool "metis_new_skolemizer" (K false)
    1.10 +val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
    1.11 +val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    1.12  
    1.13  fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
    1.14  
    1.15 @@ -190,9 +189,7 @@
    1.16                 end)))
    1.17  
    1.18  val setup =
    1.19 -  type_lits_setup
    1.20 -  #> new_skolemizer_setup
    1.21 -  #> method @{binding metis} HO "Metis for FOL/HOL problems"
    1.22 +  method @{binding metis} HO "Metis for FOL/HOL problems"
    1.23    #> method @{binding metisF} FO "Metis for FOL problems"
    1.24    #> method @{binding metisFT} FT
    1.25              "Metis for FOL/HOL problems with fully-typed translation"