1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -461,12 +461,11 @@
     1.4          val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
     1.5          val facts =
     1.6            Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
     1.7 -              Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
     1.8 +              Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
     1.9            |> filter (is_appropriate_prop o prop_of o snd)
    1.10            |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
    1.11                   (the_default default_max_relevant max_relevant)
    1.12 -                 Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts
    1.13 -                 concl_t
    1.14 +                 Sledgehammer_Fact.no_fact_override hyp_ts concl_t
    1.15          val problem =
    1.16            {state = st', goal = goal, subgoal = i,
    1.17             subgoal_count = Sledgehammer_Util.subgoal_count st,
    1.18 @@ -628,13 +627,13 @@
    1.19            #> fst
    1.20          val thms = named_thms |> maps snd
    1.21          val facts = named_thms |> map (ref_of_str o fst o fst)
    1.22 -        val relevance_override = {add = facts, del = [], only = true}
    1.23 +        val fact_override = {add = facts, del = [], only = true}
    1.24          fun my_timeout time_slice =
    1.25            timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
    1.26          fun sledge_tac time_slice prover type_enc =
    1.27            Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.28 -            (override_params prover type_enc (my_timeout time_slice))
    1.29 -            relevance_override
    1.30 +              (override_params prover type_enc (my_timeout time_slice))
    1.31 +              fact_override
    1.32        in
    1.33          if !reconstructor = "sledgehammer_tac" then
    1.34            sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_native"