src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

   |> String.translate (fn c => if Char.isPrint c then str c else "")
   |> simplify_spaces
 
 (** Structural induction rules **)
 
-fun induct_rule_on th =
+fun struct_induct_rule_on th =
   case Logic.strip_horn (prop_of th) of
     (prems, @{const Trueprop}
             $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
     if not (is_TVar ind_T) andalso length prems > 1 andalso
        exists (exists_subterm (curry (op aconv) p)) prems andalso

 fun type_match thy (T1, T2) =
   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   handle Type.TYPE_MATCH => false
 
 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, (_, th))) =
-  case induct_rule_on th of
+  case struct_induct_rule_on th of
     SOME (p_name, ind_T) =>
     let val thy = ProofContext.theory_of ctxt in
       stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
               |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
     end

       | _ => do_term t
   in Symtab.empty |> fold (do_formula pos) ts end
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   takes the given theory into account.*)
-fun theory_const_prop_of ({theory_const_rel_weight,
-                           theory_const_irrel_weight, ...} : relevance_fudge)
-                         th =
+fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
+                     : relevance_fudge) thy_name t =
   if exists (curry (op <) 0.0) [theory_const_rel_weight,
                                 theory_const_irrel_weight] then
-    let
-      val name = Context.theory_name (theory_of_thm th)
-      val t = Const (name ^ theory_const_suffix, @{typ bool})
-    in t $ prop_of th end
+    Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
   else
-    prop_of th
+    t
+
+fun theory_const_prop_of fudge th =
+  theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
 
 (**** Constant / Type Frequencies ****)
 
 (* A two-dimensional symbol table counts frequencies of constants. It's keyed
    first by constant name and second by its list of type instantiations. For the

 
 fun relevant_facts ctxt no_dangerous_types (threshold0, threshold1)
                    max_relevant is_built_in_const fudge
                    (override as {add, only, ...}) chained_ths hyp_ts concl_t =
   let
+    val thy = ProofContext.theory_of ctxt
     val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
                           1.0 / Real.fromInt (max_relevant + 1))
     val add_ths = Attrib.eval_thms ctxt add
     val reserved = reserved_isar_keyword_table ()
     val ind_stmt =

        facts
      else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
              max_relevant = 0 then
        []
      else
-       relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
-                        fudge override facts (concl_t :: hyp_ts))
+       ((concl_t |> theory_constify fudge (Context.theory_name thy)) :: hyp_ts)
+       |> relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
+                           fudge override facts)
     |> map (apfst (apfst (fn f => f ())))
   end
 
 end;