1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 27 13:52:47 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 27 13:52:47 2011 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  val proverK = "prover"
     1.5  val prover_timeoutK = "prover_timeout"
     1.6  val keepK = "keep"
     1.7 -val full_typesK = "full_types"
     1.8  val type_sysK = "type_sys"
     1.9  val slicingK = "slicing"
    1.10  val e_weight_methodK = "e_weight_method"
    1.11 @@ -630,8 +629,6 @@
    1.12    end
    1.13  
    1.14  fun invoke args =
    1.15 -  let
    1.16 -    val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
    1.17 -  in Mirabelle.register (init, sledgehammer_action args, done) end
    1.18 +  Mirabelle.register (init, sledgehammer_action args, done)
    1.19  
    1.20  end