1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 26 20:49:54 2012 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 26 20:49:54 2012 +0100
     1.3 @@ -336,7 +336,7 @@
     1.4      | NONE => get_prover (default_prover_name ()))
     1.5    end
     1.6  
     1.7 -type locality = ATP_Problem_Generate.locality
     1.8 +type stature = ATP_Problem_Generate.stature
     1.9  
    1.10  (* hack *)
    1.11  fun reconstructor_from_msg args msg =
    1.12 @@ -357,7 +357,7 @@
    1.13  local
    1.14  
    1.15  datatype sh_result =
    1.16 -  SH_OK of int * int * (string * locality) list |
    1.17 +  SH_OK of int * int * (string * stature) list |
    1.18    SH_FAIL of int * int |
    1.19    SH_ERROR
    1.20  
    1.21 @@ -486,8 +486,8 @@
    1.22      case result of
    1.23        SH_OK (time_isa, time_prover, names) =>
    1.24          let
    1.25 -          fun get_thms (name, loc) =
    1.26 -            SOME ((name, loc), thms_of_name (Proof.context_of st) name)
    1.27 +          fun get_thms (name, stature) =
    1.28 +            SOME ((name, stature), thms_of_name (Proof.context_of st) name)
    1.29          in
    1.30            change_data id inc_sh_success;
    1.31            if trivial then () else change_data id inc_sh_nontriv_success;
    1.32 @@ -654,7 +654,7 @@
    1.33          let
    1.34            val reconstructor = Unsynchronized.ref ""
    1.35            val named_thms =
    1.36 -            Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
    1.37 +            Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
    1.38            val minimize = AList.defined (op =) args minimizeK
    1.39            val metis_ft = AList.defined (op =) args metis_ftK
    1.40            val trivial =

     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 26 20:49:54 2012 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 26 20:49:54 2012 +0100
     2.3 @@ -15,8 +15,9 @@
     2.4    type formula_kind = ATP_Problem.formula_kind
     2.5    type 'a problem = 'a ATP_Problem.problem
     2.6  
     2.7 -  datatype locality =
     2.8 -    General | Induction | Intro | Elim | Simp | Local | Assum | Chained
     2.9 +  datatype scope = Global | Local | Assum | Chained
    2.10 +  datatype status = General | Induct | Intro | Elim | Simp
    2.11 +  type stature = scope * status
    2.12  
    2.13    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    2.14    datatype strictness = Strict | Non_Strict
    2.15 @@ -101,8 +102,8 @@
    2.16    val prepare_atp_problem :
    2.17      Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
    2.18      -> bool -> string -> bool -> bool -> term list -> term
    2.19 -    -> ((string * locality) * term) list
    2.20 -    -> string problem * string Symtab.table * (string * locality) list vector
    2.21 +    -> ((string * stature) * term) list
    2.22 +    -> string problem * string Symtab.table * (string * stature) list vector
    2.23         * (string * term) list * int Symtab.table
    2.24    val atp_problem_weights : string problem -> (string * real) list
    2.25  end;
    2.26 @@ -541,8 +542,9 @@
    2.27        val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
    2.28      in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
    2.29  
    2.30 -datatype locality =
    2.31 -  General | Induction | Intro | Elim | Simp | Local | Assum | Chained
    2.32 +datatype scope = Global | Local | Assum | Chained
    2.33 +datatype status = General | Induct | Intro | Elim | Simp
    2.34 +type stature = scope * status
    2.35  
    2.36  datatype order = First_Order | Higher_Order
    2.37  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    2.38 @@ -720,14 +722,14 @@
    2.39  
    2.40  type translated_formula =
    2.41    {name : string,
    2.42 -   locality : locality,
    2.43 +   stature : stature,
    2.44     kind : formula_kind,
    2.45     iformula : (name, typ, iterm) formula,
    2.46     atomic_types : typ list}
    2.47  
    2.48 -fun update_iformula f ({name, locality, kind, iformula, atomic_types}
    2.49 +fun update_iformula f ({name, stature, kind, iformula, atomic_types}
    2.50                         : translated_formula) =
    2.51 -  {name = name, locality = locality, kind = kind, iformula = f iformula,
    2.52 +  {name = name, stature = stature, kind = kind, iformula = f iformula,
    2.53     atomic_types = atomic_types} : translated_formula
    2.54  
    2.55  fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
    2.56 @@ -1180,7 +1182,8 @@
    2.57              |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
    2.58      val lam_facts =
    2.59        map2 (fn t => fn j =>
    2.60 -               ((lam_fact_prefix ^ Int.toString j, General), (Axiom, t)))
    2.61 +               ((lam_fact_prefix ^ Int.toString j, (Global, General)),
    2.62 +                (Axiom, t)))
    2.63             lambda_ts (1 upto length lambda_ts)
    2.64    in (facts, lam_facts) end
    2.65  
    2.66 @@ -1211,20 +1214,20 @@
    2.67     handle TERM _ => if role = Conjecture then @{term False} else @{term True})
    2.68    |> pair role
    2.69  
    2.70 -fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
    2.71 +fun make_formula ctxt format type_enc eq_as_iff name stature kind t =
    2.72    let
    2.73      val (iformula, atomic_Ts) =
    2.74        iformula_from_prop ctxt format type_enc eq_as_iff
    2.75                           (SOME (kind <> Conjecture)) t []
    2.76        |>> close_iformula_universally
    2.77    in
    2.78 -    {name = name, locality = loc, kind = kind, iformula = iformula,
    2.79 +    {name = name, stature = stature, kind = kind, iformula = iformula,
    2.80       atomic_types = atomic_Ts}
    2.81    end
    2.82  
    2.83 -fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
    2.84 +fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
    2.85    case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
    2.86 -                         name loc Axiom of
    2.87 +                         name stature Axiom of
    2.88      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
    2.89      if s = tptp_true then NONE else SOME formula
    2.90    | formula => SOME formula
    2.91 @@ -1234,9 +1237,10 @@
    2.92      if fastype_of t = @{typ bool} then s_not t else @{prop False} (* too meta *)
    2.93  
    2.94  fun make_conjecture ctxt format type_enc =
    2.95 -  map (fn ((name, loc), (kind, t)) =>
    2.96 +  map (fn ((name, stature), (kind, t)) =>
    2.97            t |> kind = Conjecture ? s_not_trueprop
    2.98 -            |> make_formula ctxt format type_enc (format <> CNF) name loc kind)
    2.99 +            |> make_formula ctxt format type_enc (format <> CNF) name stature
   2.100 +                            kind)
   2.101  
   2.102  (** Finite and infinite type inference **)
   2.103  
   2.104 @@ -1618,7 +1622,7 @@
   2.105              [t]
   2.106          end
   2.107          |> tag_list 1
   2.108 -        |> map (fn (k, t) => ((dub needs_fairly_sound j k, Simp), t))
   2.109 +        |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Simp)), t))
   2.110        val make_facts = map_filter (make_fact ctxt format type_enc false)
   2.111        val fairly_sound = is_type_enc_fairly_sound type_enc
   2.112      in
   2.113 @@ -1717,7 +1721,8 @@
   2.114      val conjs =
   2.115        map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
   2.116        |> map (apsnd freeze_term)
   2.117 -      |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
   2.118 +      |> map2 (pair o rpair (Local, General) o string_of_int)
   2.119 +              (0 upto length hyp_ts)
   2.120      val ((conjs, facts), lam_facts) =
   2.121        (conjs, facts)
   2.122        |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
   2.123 @@ -1892,7 +1897,7 @@
   2.124     of monomorphization). The TPTP explicitly forbids name clashes, and some of
   2.125     the remote provers might care. *)
   2.126  fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
   2.127 -        mono type_enc (j, {name, locality, kind, iformula, atomic_types}) =
   2.128 +        mono type_enc (j, {name, stature, kind, iformula, atomic_types}) =
   2.129    (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
   2.130     iformula
   2.131     |> formula_from_iformula ctxt polym_constrs format mono type_enc
   2.132 @@ -1900,7 +1905,7 @@
   2.133     |> close_formula_universally
   2.134     |> bound_tvars type_enc true atomic_types,
   2.135     NONE,
   2.136 -   case locality of
   2.137 +   case snd stature of
   2.138       Intro => isabelle_info format introN
   2.139     | Elim => isabelle_info format elimN
   2.140     | Simp => isabelle_info format simpN

     3.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 26 20:49:54 2012 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 26 20:49:54 2012 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4    type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
     3.5    type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
     3.6    type 'a proof = 'a ATP_Proof.proof
     3.7 -  type locality = ATP_Problem_Generate.locality
     3.8 +  type stature = ATP_Problem_Generate.stature
     3.9  
    3.10    datatype reconstructor =
    3.11      Metis of string * string |
    3.12 @@ -24,9 +24,9 @@
    3.13  
    3.14    type minimize_command = string list -> string
    3.15    type one_line_params =
    3.16 -    play * string * (string * locality) list * minimize_command * int * int
    3.17 +    play * string * (string * stature) list * minimize_command * int * int
    3.18    type isar_params =
    3.19 -    bool * int * string Symtab.table * (string * locality) list vector
    3.20 +    bool * int * string Symtab.table * (string * stature) list vector
    3.21      * int Symtab.table * string proof * thm
    3.22  
    3.23    val metisN : string
    3.24 @@ -44,12 +44,12 @@
    3.25    val metis_call : string -> string -> string
    3.26    val string_for_reconstructor : reconstructor -> string
    3.27    val used_facts_in_atp_proof :
    3.28 -    Proof.context -> (string * locality) list vector -> string proof
    3.29 -    -> (string * locality) list
    3.30 +    Proof.context -> (string * stature) list vector -> string proof
    3.31 +    -> (string * stature) list
    3.32    val lam_trans_from_atp_proof : string proof -> string -> string
    3.33    val is_typed_helper_used_in_atp_proof : string proof -> bool
    3.34    val used_facts_in_unsound_atp_proof :
    3.35 -    Proof.context -> (string * locality) list vector -> 'a proof
    3.36 +    Proof.context -> (string * stature) list vector -> 'a proof
    3.37      -> string list option
    3.38    val unalias_type_enc : string -> string list
    3.39    val one_line_proof_text : one_line_params -> string
    3.40 @@ -93,9 +93,9 @@
    3.41  
    3.42  type minimize_command = string list -> string
    3.43  type one_line_params =
    3.44 -  play * string * (string * locality) list * minimize_command * int * int
    3.45 +  play * string * (string * stature) list * minimize_command * int * int
    3.46  type isar_params =
    3.47 -  bool * int * string Symtab.table * (string * locality) list vector
    3.48 +  bool * int * string Symtab.table * (string * stature) list vector
    3.49    * int Symtab.table * string proof * thm
    3.50  
    3.51  val metisN = "metis"
    3.52 @@ -198,25 +198,20 @@
    3.53  fun add_fact _ fact_names (Inference ((_, ss), _, _, [])) =
    3.54      union (op =) (resolve_fact fact_names ss)
    3.55    | add_fact ctxt _ (Inference (_, _, rule, _)) =
    3.56 -    if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I
    3.57 +    if rule = leo2_ext then insert (op =) (ext_name ctxt, (Global, General))
    3.58 +    else I
    3.59    | add_fact _ _ _ = I
    3.60  
    3.61  fun used_facts_in_atp_proof ctxt fact_names atp_proof =
    3.62    if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
    3.63    else fold (add_fact ctxt fact_names) atp_proof []
    3.64  
    3.65 -(* (quasi-)underapproximation of the truth *)
    3.66 -fun is_locality_global Local = false
    3.67 -  | is_locality_global Assum = false
    3.68 -  | is_locality_global Chained = false
    3.69 -  | is_locality_global _ = true
    3.70 -
    3.71  fun used_facts_in_unsound_atp_proof _ _ [] = NONE
    3.72    | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
    3.73      let
    3.74        val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
    3.75      in
    3.76 -      if forall (is_locality_global o snd) used_facts andalso
    3.77 +      if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
    3.78           not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
    3.79          SOME (map fst used_facts)
    3.80        else
    3.81 @@ -250,10 +245,11 @@
    3.82    | minimize_line minimize_command ss =
    3.83      case minimize_command ss of
    3.84        "" => ""
    3.85 -    | command => "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
    3.86 +    | command =>
    3.87 +      "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
    3.88  
    3.89  val split_used_facts =
    3.90 -  List.partition (curry (op =) Chained o snd)
    3.91 +  List.partition (fn (_, (sc, _)) => sc = Chained)
    3.92    #> pairself (sort_distinct (string_ord o pairself fst))
    3.93  
    3.94  fun one_line_proof_text (preplay, banner, used_facts, minimize_command,

     4.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Thu Jan 26 20:49:54 2012 +0100
     4.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Thu Jan 26 20:49:54 2012 +0100
     4.3 @@ -222,10 +222,9 @@
     4.4          |> pairself (maps (map (zero_var_indexes o snd)))
     4.5      val num_conjs = length conj_clauses
     4.6      val clauses =
     4.7 -      map2 (fn j => pair (Int.toString j, Local))
     4.8 +      map2 (fn j => pair (Int.toString j, (Local, General)))
     4.9             (0 upto num_conjs - 1) conj_clauses @
    4.10 -      (* "General" below isn't quite correct; the fact could be local. *)
    4.11 -      map2 (fn j => pair (Int.toString (num_conjs + j), General))
    4.12 +      map2 (fn j => pair (Int.toString (num_conjs + j), (Local, General)))
    4.13             (0 upto length fact_clauses - 1) fact_clauses
    4.14      val (old_skolems, props) =
    4.15        fold_rev (fn (name, th) => fn (old_skolems, props) =>

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jan 26 20:49:54 2012 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jan 26 20:49:54 2012 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  signature SLEDGEHAMMER_FILTER =
     5.6  sig
     5.7 -  type locality = ATP_Problem_Generate.locality
     5.8 +  type stature = ATP_Problem_Generate.stature
     5.9  
    5.10    type relevance_fudge =
    5.11      {local_const_multiplier : real,
    5.12 @@ -44,19 +44,19 @@
    5.13      -> string list
    5.14    val fact_from_ref :
    5.15      Proof.context -> unit Symtab.table -> thm list
    5.16 -    -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
    5.17 +    -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    5.18    val all_facts :
    5.19      Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
    5.20 -    -> (((unit -> string) * locality) * thm) list
    5.21 +    -> (((unit -> string) * stature) * thm) list
    5.22    val nearly_all_facts :
    5.23      Proof.context -> bool -> relevance_override -> thm list -> term list -> term
    5.24 -    -> (((unit -> string) * locality) * thm) list
    5.25 +    -> (((unit -> string) * stature) * thm) list
    5.26    val relevant_facts :
    5.27      Proof.context -> real * real -> int
    5.28      -> (string * typ -> term list -> bool * term list) -> relevance_fudge
    5.29      -> relevance_override -> thm list -> term list -> term
    5.30 -    -> (((unit -> string) * locality) * thm) list
    5.31 -    -> ((string * locality) * thm) list
    5.32 +    -> (((unit -> string) * stature) * thm) list
    5.33 +    -> ((string * stature) * thm) list
    5.34  end;
    5.35  
    5.36  structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
    5.37 @@ -144,8 +144,8 @@
    5.38      |-> fold (fn th => fn (j, rest) =>
    5.39                   (j + 1,
    5.40                    ((nth_name j,
    5.41 -                    if member Thm.eq_thm_prop chained_ths th then Chained
    5.42 -                    else General), th) :: rest))
    5.43 +                    (if member Thm.eq_thm_prop chained_ths th then Chained
    5.44 +                     else Local (* just in case *), General)), th) :: rest))
    5.45      |> snd
    5.46    end
    5.47  
    5.48 @@ -190,7 +190,7 @@
    5.49        NONE
    5.50    | _ => NONE
    5.51  
    5.52 -fun instantiate_induct_rule ctxt concl_prop p_name ((name, loc), th) ind_x =
    5.53 +fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
    5.54    let
    5.55      fun varify_noninducts (t as Free (s, T)) =
    5.56          if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
    5.57 @@ -200,8 +200,8 @@
    5.58                   |> lambda (Free ind_x)
    5.59                   |> string_for_term ctxt
    5.60    in
    5.61 -    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", loc),
    5.62 -     th |> read_instantiate ctxt [((p_name, 0), p_inst)])
    5.63 +    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
    5.64 +      stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
    5.65    end
    5.66  
    5.67  fun type_match thy (T1, T2) =
    5.68 @@ -467,19 +467,21 @@
    5.69                          chained_const_irrel_weight (irrel_weight_for fudge) swap
    5.70                          const_tab chained_const_tab
    5.71  
    5.72 -fun locality_bonus ({intro_bonus, ...} : relevance_fudge) Intro = intro_bonus
    5.73 -  | locality_bonus {elim_bonus, ...} Elim = elim_bonus
    5.74 -  | locality_bonus {simp_bonus, ...} Simp = simp_bonus
    5.75 -  | locality_bonus {local_bonus, ...} Local = local_bonus
    5.76 -  | locality_bonus {assum_bonus, ...} Assum = assum_bonus
    5.77 -  | locality_bonus {chained_bonus, ...} Chained = chained_bonus
    5.78 -  | locality_bonus _ _ = 0.0
    5.79 +fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
    5.80 +    intro_bonus
    5.81 +  | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
    5.82 +  | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
    5.83 +  | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
    5.84 +  | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
    5.85 +  | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
    5.86 +  | stature_bonus _ _ = 0.0
    5.87  
    5.88  fun is_odd_const_name s =
    5.89    s = abs_name orelse String.isPrefix skolem_prefix s orelse
    5.90    String.isSuffix theory_const_suffix s
    5.91  
    5.92 -fun fact_weight fudge loc const_tab relevant_consts chained_consts fact_consts =
    5.93 +fun fact_weight fudge stature const_tab relevant_consts chained_consts
    5.94 +                fact_consts =
    5.95    case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
    5.96                     ||> filter_out (pconst_hyper_mem swap relevant_consts) of
    5.97      ([], _) => 0.0
    5.98 @@ -492,7 +494,7 @@
    5.99          val rel_weight =
   5.100            0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
   5.101          val irrel_weight =
   5.102 -          ~ (locality_bonus fudge loc)
   5.103 +          ~ (stature_bonus fudge stature)
   5.104            |> fold (curry (op +)
   5.105                     o irrel_pconst_weight fudge const_tab chained_consts) irrel
   5.106          val res = rel_weight / (rel_weight + irrel_weight)
   5.107 @@ -512,7 +514,7 @@
   5.108  val const_names_in_fact = map fst ooo pconsts_in_fact
   5.109  
   5.110  type annotated_thm =
   5.111 -  (((unit -> string) * locality) * thm) * (string * ptype) list
   5.112 +  (((unit -> string) * stature) * thm) * (string * ptype) list
   5.113  
   5.114  fun take_most_relevant ctxt max_relevant remaining_max
   5.115          ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
   5.116 @@ -537,13 +539,12 @@
   5.117      (accepts, more_rejects @ rejects)
   5.118    end
   5.119  
   5.120 -fun if_empty_replace_with_locality thy is_built_in_const facts loc tab =
   5.121 +fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
   5.122    if Symtab.is_empty tab then
   5.123      Symtab.empty
   5.124      |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
   5.125 -            (map_filter (fn ((_, loc'), th) =>
   5.126 -                            if loc' = loc then SOME (prop_of th) else NONE)
   5.127 -                        facts)
   5.128 +            (map_filter (fn ((_, (sc', _)), th) =>
   5.129 +                            if sc' = sc then SOME (prop_of th) else NONE) facts)
   5.130    else
   5.131      tab
   5.132  
   5.133 @@ -584,7 +585,7 @@
   5.134        Symtab.empty |> fold (add_pconsts true) hyp_ts
   5.135                     |> add_pconsts false concl_t
   5.136        |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
   5.137 -      |> fold (if_empty_replace_with_locality thy is_built_in_const facts)
   5.138 +      |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
   5.139                [Chained, Assum, Local]
   5.140      val add_ths = Attrib.eval_thms ctxt add
   5.141      val del_ths = Attrib.eval_thms ctxt del
   5.142 @@ -637,13 +638,13 @@
   5.143                        hopeless_rejects hopeful_rejects)
   5.144              end
   5.145            | relevant candidates rejects
   5.146 -                     (((ax as (((_, loc), _), fact_consts)), cached_weight)
   5.147 +                     (((ax as (((_, stature), _), fact_consts)), cached_weight)
   5.148                        :: hopeful) =
   5.149              let
   5.150                val weight =
   5.151                  case cached_weight of
   5.152                    SOME w => w
   5.153 -                | NONE => fact_weight fudge loc const_tab rel_const_tab
   5.154 +                | NONE => fact_weight fudge stature const_tab rel_const_tab
   5.155                                        chained_const_tab fact_consts
   5.156              in
   5.157                if weight >= threshold then
   5.158 @@ -783,8 +784,8 @@
   5.159    let
   5.160      val thy = Proof_Context.theory_of ctxt
   5.161      val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
   5.162 -    fun add loc g f =
   5.163 -      fold (Termtab.update o rpair loc o g o crude_zero_vars o prop_of o f)
   5.164 +    fun add stature g f =
   5.165 +      fold (Termtab.update o rpair stature o g o crude_zero_vars o prop_of o f)
   5.166      val {safeIs, safeEs, hazIs, hazEs, ...} =
   5.167        ctxt |> claset_of |> Classical.rep_cs
   5.168      val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   5.169 @@ -809,20 +810,19 @@
   5.170      fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
   5.171      val is_chained = member Thm.eq_thm_prop chained_ths
   5.172      val clasimpset_table = clasimpset_rule_table_of ctxt
   5.173 -    fun locality_of_theorem global name th =
   5.174 -      if String.isSubstring ".induct" name orelse (*FIXME: use structured name*)
   5.175 +    fun scope_of_thm global th =
   5.176 +      if is_chained th then Chained
   5.177 +      else if global then Global
   5.178 +      else if is_assum th then Assum
   5.179 +      else Local
   5.180 +    fun status_of_thm name th =
   5.181 +      (* FIXME: use structured name *)
   5.182 +      if String.isSubstring ".induct" name orelse
   5.183           String.isSubstring ".inducts" name then
   5.184 -        Induction
   5.185 -      else if is_chained th then
   5.186 -        Chained
   5.187 -      else if global then
   5.188 -        case Termtab.lookup clasimpset_table (prop_of th) of
   5.189 -          SOME loc => loc
   5.190 -        | NONE => General
   5.191 -      else if is_assum th then
   5.192 -        Assum
   5.193 -      else
   5.194 -        Local
   5.195 +        Induct
   5.196 +      else case Termtab.lookup clasimpset_table (prop_of th) of
   5.197 +        SOME status => status
   5.198 +      | NONE => General
   5.199      fun is_good_unnamed_local th =
   5.200        not (Thm.has_name_hint th) andalso
   5.201        forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   5.202 @@ -872,7 +872,8 @@
   5.203                                     |> (fn SOME name =>
   5.204                                            make_name reserved multi j name
   5.205                                          | NONE => "")),
   5.206 -                                locality_of_theorem global name0 th), th)
   5.207 +                                (scope_of_thm global th,
   5.208 +                                 status_of_thm name0 th)), th)
   5.209                             in
   5.210                               if multi then (new :: multis, unis)
   5.211                               else (multis, new :: unis)
   5.212 @@ -902,7 +903,7 @@
   5.213      val ind_stmt_xs = external_frees ind_stmt
   5.214    in
   5.215      (if only then
   5.216 -       maps (map (fn ((name, loc), th) => ((K name, loc), th))
   5.217 +       maps (map (fn ((name, stature), th) => ((K name, stature), th))
   5.218               o fact_from_ref ctxt reserved chained_ths) add
   5.219       else
   5.220         all_facts ctxt ho_atp reserved false add_ths chained_ths)

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Jan 26 20:49:54 2012 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Jan 26 20:49:54 2012 +0100
     6.3 @@ -7,15 +7,15 @@
     6.4  
     6.5  signature SLEDGEHAMMER_MINIMIZE =
     6.6  sig
     6.7 -  type locality = ATP_Problem_Generate.locality
     6.8 +  type stature = ATP_Problem_Generate.stature
     6.9    type play = ATP_Proof_Reconstruct.play
    6.10    type params = Sledgehammer_Provers.params
    6.11  
    6.12    val binary_min_facts : int Config.T
    6.13    val minimize_facts :
    6.14      string -> params -> bool -> int -> int -> Proof.state
    6.15 -    -> ((string * locality) * thm list) list
    6.16 -    -> ((string * locality) * thm list) list option
    6.17 +    -> ((string * stature) * thm list) list
    6.18 +    -> ((string * stature) * thm list) list option
    6.19         * ((unit -> play) * (play -> string) * string)
    6.20    val run_minimize :
    6.21      params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
    6.22 @@ -192,7 +192,8 @@
    6.23             min test (new_timeout timeout run_time) result facts
    6.24           val _ = print silent (fn () => cat_lines
    6.25             ["Minimized to " ^ n_facts (map fst min_facts)] ^
    6.26 -            (case length (filter (curry (op =) Chained o snd o fst) min_facts) of
    6.27 +            (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
    6.28 +                            |> length of
    6.29                 0 => ""
    6.30               | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
    6.31         in (SOME min_facts, (preplay, message, message_tail)) end

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 26 20:49:54 2012 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 26 20:49:54 2012 +0100
     7.3 @@ -9,7 +9,7 @@
     7.4  signature SLEDGEHAMMER_PROVERS =
     7.5  sig
     7.6    type failure = ATP_Proof.failure
     7.7 -  type locality = ATP_Problem_Generate.locality
     7.8 +  type stature = ATP_Problem_Generate.stature
     7.9    type type_enc = ATP_Problem_Generate.type_enc
    7.10    type reconstructor = ATP_Proof_Reconstruct.reconstructor
    7.11    type play = ATP_Proof_Reconstruct.play
    7.12 @@ -40,8 +40,8 @@
    7.13       expect: string}
    7.14  
    7.15    datatype prover_fact =
    7.16 -    Untranslated_Fact of (string * locality) * thm |
    7.17 -    SMT_Weighted_Fact of (string * locality) * (int option * thm)
    7.18 +    Untranslated_Fact of (string * stature) * thm |
    7.19 +    SMT_Weighted_Fact of (string * stature) * (int option * thm)
    7.20  
    7.21    type prover_problem =
    7.22      {state: Proof.state,
    7.23 @@ -49,11 +49,11 @@
    7.24       subgoal: int,
    7.25       subgoal_count: int,
    7.26       facts: prover_fact list,
    7.27 -     smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
    7.28 +     smt_filter: (string * stature) SMT_Solver.smt_filter_data option}
    7.29  
    7.30    type prover_result =
    7.31      {outcome: failure option,
    7.32 -     used_facts: (string * locality) list,
    7.33 +     used_facts: (string * stature) list,
    7.34       run_time: Time.time,
    7.35       preplay: unit -> play,
    7.36       message: play -> string,
    7.37 @@ -98,12 +98,12 @@
    7.38    val smt_relevance_fudge : relevance_fudge
    7.39    val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
    7.40    val weight_smt_fact :
    7.41 -    Proof.context -> int -> ((string * locality) * thm) * int
    7.42 -    -> (string * locality) * (int option * thm)
    7.43 -  val untranslated_fact : prover_fact -> (string * locality) * thm
    7.44 +    Proof.context -> int -> ((string * stature) * thm) * int
    7.45 +    -> (string * stature) * (int option * thm)
    7.46 +  val untranslated_fact : prover_fact -> (string * stature) * thm
    7.47    val smt_weighted_fact :
    7.48      Proof.context -> int -> prover_fact * int
    7.49 -    -> (string * locality) * (int option * thm)
    7.50 +    -> (string * stature) * (int option * thm)
    7.51    val supported_provers : Proof.context -> unit
    7.52    val kill_provers : unit -> unit
    7.53    val running_provers : unit -> unit
    7.54 @@ -304,8 +304,8 @@
    7.55     expect: string}
    7.56  
    7.57  datatype prover_fact =
    7.58 -  Untranslated_Fact of (string * locality) * thm |
    7.59 -  SMT_Weighted_Fact of (string * locality) * (int option * thm)
    7.60 +  Untranslated_Fact of (string * stature) * thm |
    7.61 +  SMT_Weighted_Fact of (string * stature) * (int option * thm)
    7.62  
    7.63  type prover_problem =
    7.64    {state: Proof.state,
    7.65 @@ -313,11 +313,11 @@
    7.66     subgoal: int,
    7.67     subgoal_count: int,
    7.68     facts: prover_fact list,
    7.69 -   smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
    7.70 +   smt_filter: (string * stature) SMT_Solver.smt_filter_data option}
    7.71  
    7.72  type prover_result =
    7.73    {outcome: failure option,
    7.74 -   used_facts: (string * locality) list,
    7.75 +   used_facts: (string * stature) list,
    7.76     run_time: Time.time,
    7.77     preplay: unit -> play,
    7.78     message: play -> string,

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 26 20:49:54 2012 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 26 20:49:54 2012 +0100
     8.3 @@ -172,7 +172,7 @@
     8.4    get_prover ctxt mode name params minimize_command problem
     8.5    |> minimize ctxt mode name params problem
     8.6  
     8.7 -fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
     8.8 +fun is_induction_fact (Untranslated_Fact ((_, (_, Induct)), _)) = true
     8.9    | is_induction_fact _ = false
    8.10  
    8.11  fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,