1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -45,18 +45,14 @@
     1.4  
     1.5  (** Sledgehammer commands **)
     1.6  
     1.7 -fun add_relevance_override ns : relevance_override =
     1.8 -  {add = ns, del = [], only = false}
     1.9 -fun del_relevance_override ns : relevance_override =
    1.10 -  {add = [], del = ns, only = false}
    1.11 -fun only_relevance_override ns : relevance_override =
    1.12 -  {add = ns, del = [], only = true}
    1.13 -fun merge_relevance_override_pairwise (r1 : relevance_override)
    1.14 -                                      (r2 : relevance_override) =
    1.15 +fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
    1.16 +fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
    1.17 +fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
    1.18 +fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
    1.19    {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    1.20     only = #only r1 andalso #only r2}
    1.21 -fun merge_relevance_overrides rs =
    1.22 -  fold merge_relevance_override_pairwise rs (only_relevance_override [])
    1.23 +fun merge_fact_overrides rs =
    1.24 +  fold merge_fact_override_pairwise rs (only_fact_override [])
    1.25  
    1.26  (*** parameters ***)
    1.27  
    1.28 @@ -350,7 +346,7 @@
    1.29      (if i = 1 then "" else " " ^ string_of_int i)
    1.30    end
    1.31  
    1.32 -fun hammer_away override_params subcommand opt_i relevance_override state =
    1.33 +fun hammer_away override_params subcommand opt_i fact_override state =
    1.34    let
    1.35      val ctxt = Proof.context_of state
    1.36      val override_params = override_params |> map (normalize_raw_param ctxt)
    1.37 @@ -358,7 +354,7 @@
    1.38      if subcommand = runN then
    1.39        let val i = the_default 1 opt_i in
    1.40          run_sledgehammer (get_params Normal ctxt override_params) Normal i
    1.41 -                         relevance_override (minimize_command override_params i)
    1.42 +                         fact_override (minimize_command override_params i)
    1.43                           state
    1.44          |> K ()
    1.45        end
    1.46 @@ -366,7 +362,7 @@
    1.47        run_minimize (get_params Minimize ctxt
    1.48                                 (("provers", [default_minimize_prover]) ::
    1.49                                  override_params))
    1.50 -                   (the_default 1 opt_i) (#add relevance_override) state
    1.51 +                   (the_default 1 opt_i) (#add fact_override) state
    1.52      else if subcommand = messagesN then
    1.53        messages opt_i
    1.54      else if subcommand = supported_proversN then
    1.55 @@ -381,8 +377,8 @@
    1.56        error ("Unknown subcommand: " ^ quote subcommand ^ ".")
    1.57    end
    1.58  
    1.59 -fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
    1.60 -  Toplevel.keep (hammer_away params subcommand opt_i relevance_override
    1.61 +fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
    1.62 +  Toplevel.keep (hammer_away params subcommand opt_i fact_override
    1.63                   o Toplevel.proof_of)
    1.64  
    1.65  fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value
    1.66 @@ -410,19 +406,19 @@
    1.67  val parse_fact_refs =
    1.68    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
    1.69  val parse_relevance_chunk =
    1.70 -  (Args.add |-- Args.colon |-- parse_fact_refs >> add_relevance_override)
    1.71 -  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_relevance_override)
    1.72 -  || (parse_fact_refs >> only_relevance_override)
    1.73 -val parse_relevance_override =
    1.74 +  (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
    1.75 +  || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
    1.76 +  || (parse_fact_refs >> only_fact_override)
    1.77 +val parse_fact_override =
    1.78    Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
    1.79 -                              >> merge_relevance_overrides))
    1.80 -                no_relevance_override
    1.81 +                              >> merge_fact_overrides))
    1.82 +                no_fact_override
    1.83  
    1.84  val _ =
    1.85    Outer_Syntax.improper_command @{command_spec "sledgehammer"}
    1.86      "search for first-order proof using automatic theorem provers"
    1.87      ((Scan.optional Parse.short_ident runN -- parse_params
    1.88 -      -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
    1.89 +      -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
    1.90  val _ =
    1.91    Outer_Syntax.command @{command_spec "sledgehammer_params"}
    1.92      "set and display the default parameters for Sledgehammer"
    1.93 @@ -434,7 +430,7 @@
    1.94      val mode = if auto then Auto_Try else Try
    1.95      val i = 1
    1.96    in
    1.97 -    run_sledgehammer (get_params mode ctxt []) mode i no_relevance_override
    1.98 +    run_sledgehammer (get_params mode ctxt []) mode i no_fact_override
    1.99                       (minimize_command [] i) state
   1.100    end
   1.101