src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
author blanchet
Thu Jan 10 23:34:20 2013 +0100 (2013-01-10 ago)
changeset 50815 41b804049fae
parent 50756 c96bb430ddb0
child 51004 5f2788c38127
permissions -rw-r--r--
make name table work the way it was intended to
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Sledgehammer fact handling.
     6 *)
     7 
     8 signature SLEDGEHAMMER_FACT =
     9 sig
    10   type status = ATP_Problem_Generate.status
    11   type stature = ATP_Problem_Generate.stature
    12 
    13   type fact = ((unit -> string) * stature) * thm
    14 
    15   type fact_override =
    16     {add : (Facts.ref * Attrib.src list) list,
    17      del : (Facts.ref * Attrib.src list) list,
    18      only : bool}
    19 
    20   val ignore_no_atp : bool Config.T
    21   val instantiate_inducts : bool Config.T
    22   val no_fact_override : fact_override
    23   val fact_from_ref :
    24     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
    25     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    26   val backquote_thm : Proof.context -> thm -> string
    27   val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
    28   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    29   val build_name_tables :
    30     (thm -> string) -> ('a * thm) list
    31     -> string Symtab.table * string Symtab.table
    32   val maybe_instantiate_inducts :
    33     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    34     -> (((unit -> string) * 'a) * thm) list
    35   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    36   val all_facts :
    37     Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
    38     -> status Termtab.table -> fact list
    39   val nearly_all_facts :
    40     Proof.context -> bool -> fact_override -> unit Symtab.table
    41     -> status Termtab.table -> thm list -> term list -> term -> fact list
    42 end;
    43 
    44 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    45 struct
    46 
    47 open ATP_Util
    48 open ATP_Problem_Generate
    49 open Metis_Tactic
    50 open Sledgehammer_Util
    51 
    52 type fact = ((unit -> string) * stature) * thm
    53 
    54 type fact_override =
    55   {add : (Facts.ref * Attrib.src list) list,
    56    del : (Facts.ref * Attrib.src list) list,
    57    only : bool}
    58 
    59 (* experimental features *)
    60 val ignore_no_atp =
    61   Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
    62 val instantiate_inducts =
    63   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    64 
    65 val no_fact_override = {add = [], del = [], only = false}
    66 
    67 fun needs_quoting reserved s =
    68   Symtab.defined reserved s orelse
    69   exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
    70 
    71 fun make_name reserved multi j name =
    72   (name |> needs_quoting reserved name ? quote) ^
    73   (if multi then "(" ^ string_of_int j ^ ")" else "")
    74 
    75 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    76   | explode_interval max (Facts.From i) = i upto i + max - 1
    77   | explode_interval _ (Facts.Single i) = [i]
    78 
    79 val backquote =
    80   raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
    81 
    82 (* unfolding these can yield really huge terms *)
    83 val risky_defs = @{thms Bit0_def Bit1_def}
    84 
    85 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    86 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    87   | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    88   | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    89   | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
    90   | is_rec_def _ = false
    91 
    92 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
    93 fun is_chained chained = member Thm.eq_thm_prop chained
    94 
    95 fun scope_of_thm global assms chained th =
    96   if is_chained chained th then Chained
    97   else if global then Global
    98   else if is_assum assms th then Assum
    99   else Local
   100 
   101 val may_be_induction =
   102   exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
   103                      body_type T = @{typ bool}
   104                    | _ => false)
   105 
   106 fun status_of_thm css name th =
   107   (* FIXME: use structured name *)
   108   if (String.isSubstring ".induct" name orelse
   109       String.isSubstring ".inducts" name) andalso
   110      may_be_induction (prop_of th) then
   111     Induction
   112   else case Termtab.lookup css (prop_of th) of
   113     SOME status => status
   114   | NONE => General
   115 
   116 fun stature_of_thm global assms chained css name th =
   117   (scope_of_thm global assms chained th, status_of_thm css name th)
   118 
   119 fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
   120   let
   121     val ths = Attrib.eval_thms ctxt [xthm]
   122     val bracket =
   123       map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
   124       |> implode
   125     fun nth_name j =
   126       case xref of
   127         Facts.Fact s => backquote s ^ bracket
   128       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
   129       | Facts.Named ((name, _), NONE) =>
   130         make_name reserved (length ths > 1) (j + 1) name ^ bracket
   131       | Facts.Named ((name, _), SOME intervals) =>
   132         make_name reserved true
   133                  (nth (maps (explode_interval (length ths)) intervals) j) name ^
   134         bracket
   135     fun add_nth th (j, rest) =
   136       let val name = nth_name j in
   137         (j + 1, ((name, stature_of_thm false [] chained css name th), th)
   138                 :: rest)
   139       end
   140   in (0, []) |> fold add_nth ths |> snd end
   141 
   142 (* Reject theorems with names like "List.filter.filter_list_def" or
   143   "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
   144 fun is_package_def s =
   145   let val ss = Long_Name.explode s in
   146     length ss > 2 andalso not (hd ss = "local") andalso
   147     exists (fn suf => String.isSuffix suf s)
   148            ["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
   149   end
   150 
   151 (* FIXME: put other record thms here, or declare as "no_atp" *)
   152 fun multi_base_blacklist ctxt ho_atp =
   153   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
   154    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
   155    "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
   156    "nibble.distinct"]
   157   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
   158         append ["induct", "inducts"]
   159   |> map (prefix Long_Name.separator)
   160 
   161 val max_lambda_nesting = 5 (*only applies if not ho_atp*)
   162 
   163 fun term_has_too_many_lambdas max (t1 $ t2) =
   164     exists (term_has_too_many_lambdas max) [t1, t2]
   165   | term_has_too_many_lambdas max (Abs (_, _, t)) =
   166     max = 0 orelse term_has_too_many_lambdas (max - 1) t
   167   | term_has_too_many_lambdas _ _ = false
   168 
   169 (* Don't count nested lambdas at the level of formulas, since they are
   170    quantifiers. *)
   171 fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
   172     formula_has_too_many_lambdas (T :: Ts) t
   173   | formula_has_too_many_lambdas Ts t =
   174     if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
   175       exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
   176     else
   177       term_has_too_many_lambdas max_lambda_nesting t
   178 
   179 (* The maximum apply depth of any "metis" call in "Metis_Examples" (on
   180    2007-10-31) was 11. *)
   181 val max_apply_depth = 18
   182 
   183 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   184   | apply_depth (Abs (_, _, t)) = apply_depth t
   185   | apply_depth _ = 0
   186 
   187 fun is_too_complex ho_atp t =
   188   apply_depth t > max_apply_depth orelse
   189   (not ho_atp andalso formula_has_too_many_lambdas [] t)
   190 
   191 (* FIXME: Ad hoc list *)
   192 val technical_prefixes =
   193   ["ATP", "Code_Evaluation", "Datatype", "DSequence", "Enum", "Lazy_Sequence",
   194    "Meson", "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence",
   195    "Quickcheck", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
   196    "Random_Sequence", "Sledgehammer", "SMT"]
   197   |> map (suffix Long_Name.separator)
   198 
   199 fun has_technical_prefix s =
   200   exists (fn pref => String.isPrefix pref s) technical_prefixes
   201 val exists_technical_const = exists_Const (has_technical_prefix o fst)
   202 
   203 (* FIXME: make more reliable *)
   204 val exists_low_level_class_const =
   205   exists_Const (fn (s, _) =>
   206      s = @{const_name equal_class.equal} orelse
   207      String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
   208 
   209 fun is_that_fact th =
   210   String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
   211   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
   212                            | _ => false) (prop_of th)
   213 
   214 fun is_likely_tautology_too_meta_or_too_technical th =
   215   let
   216     fun is_interesting_subterm (Const (s, _)) =
   217         not (member (op =) atp_widely_irrelevant_consts s)
   218       | is_interesting_subterm (Free _) = true
   219       | is_interesting_subterm _ = false
   220     fun is_boring_bool t =
   221       not (exists_subterm is_interesting_subterm t) orelse
   222       exists_type (exists_subtype (curry (op =) @{typ prop})) t
   223     fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
   224       | is_boring_prop Ts (@{const "==>"} $ t $ u) =
   225         is_boring_prop Ts t andalso is_boring_prop Ts u
   226       | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
   227         is_boring_prop (T :: Ts) t
   228       | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
   229         is_boring_prop Ts (t $ eta_expand Ts u 1)
   230       | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
   231         is_boring_bool t andalso is_boring_bool u
   232       | is_boring_prop _ _ = true
   233     val t = prop_of th
   234   in
   235     (is_boring_prop [] (prop_of th) andalso
   236      not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
   237     exists_type type_has_top_sort t orelse exists_technical_const t orelse
   238     exists_low_level_class_const t orelse is_that_fact th
   239   end
   240 
   241 fun is_blacklisted_or_something ctxt ho_atp name =
   242   (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
   243   exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
   244 
   245 fun hackish_string_for_term ctxt =
   246   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   247 
   248 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   249    they are displayed as "M" and we want to avoid clashes with these. But
   250    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   251    prefixes of all free variables. In the worse case scenario, where the fact
   252    won't be resolved correctly, the user can fix it manually, e.g., by giving a
   253    name to the offending fact. *)
   254 fun all_prefixes_of s =
   255   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   256 
   257 fun close_form t =
   258   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   259   |> fold (fn ((s, i), T) => fn (t', taken) =>
   260               let val s' = singleton (Name.variant_list taken) s in
   261                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   262                   else Logic.all_const) T
   263                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
   264                  s' :: taken)
   265               end)
   266           (Term.add_vars t [] |> sort_wrt (fst o fst))
   267   |> fst
   268 
   269 fun backquote_term ctxt t =
   270   t |> close_form
   271     |> hackish_string_for_term ctxt
   272     |> backquote
   273 
   274 fun backquote_thm ctxt th = backquote_term ctxt (prop_of th)
   275 
   276 fun clasimpset_rule_table_of ctxt =
   277   let
   278     val thy = Proof_Context.theory_of ctxt
   279     val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
   280     fun add stature normalizers get_th =
   281       fold (fn rule =>
   282                let
   283                  val th = rule |> get_th
   284                  val t =
   285                    th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
   286                in
   287                  fold (fn normalize => Termtab.update (normalize t, stature))
   288                       (I :: normalizers)
   289                end)
   290     val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
   291       ctxt |> claset_of |> Classical.rep_cs
   292     val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   293 (* Add once it is used:
   294     val elims =
   295       Item_Net.content safeEs @ Item_Net.content hazEs
   296       |> map Classical.classical_rule
   297 *)
   298     val simps = ctxt |> simpset_of |> dest_ss |> #simps
   299     val specs = ctxt |> Spec_Rules.get
   300     val (rec_defs, nonrec_defs) =
   301       specs |> filter (curry (op =) Spec_Rules.Equational o fst)
   302             |> maps (snd o snd)
   303             |> filter_out (member Thm.eq_thm_prop risky_defs)
   304             |> List.partition (is_rec_def o prop_of)
   305     val spec_intros =
   306       specs |> filter (member (op =) [Spec_Rules.Inductive,
   307                                       Spec_Rules.Co_Inductive] o fst)
   308             |> maps (snd o snd)
   309   in
   310     Termtab.empty |> add Simp [atomize] snd simps
   311                   |> add Rec_Def [] I rec_defs
   312                   |> add Non_Rec_Def [] I nonrec_defs
   313 (* Add once it is used:
   314                   |> add Elim [] I elims
   315 *)
   316                   |> add Intro [] I intros
   317                   |> add Inductive [] I spec_intros
   318   end
   319 
   320 fun normalize_eq (t as @{const Trueprop}
   321         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
   322     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   323     else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
   324   | normalize_eq (t as @{const Trueprop} $ (@{const Not}
   325         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   326     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   327     else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
   328   | normalize_eq t = t
   329 
   330 val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes
   331 
   332 fun if_thm_before th th' =
   333   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
   334 
   335 (* Hack: Conflate the facts about a class as seen from the outside with the
   336    corresponding low-level facts, so that MaSh can learn from the low-level
   337    proofs. *)
   338 fun un_class_ify s =
   339   case first_field "_class" s of
   340     SOME (pref, suf) => [s, pref ^ suf]
   341   | NONE => [s]
   342 
   343 fun build_name_tables name_of facts =
   344   let
   345     fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
   346     fun add_plain canon alias =
   347       Symtab.update (Thm.get_name_hint alias,
   348                      name_of (if_thm_before canon alias))
   349     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
   350     fun add_inclass (name, target) =
   351       fold (fn s => Symtab.update (s, target)) (un_class_ify name)
   352     val prop_tab = fold cons_thm facts Termtab.empty
   353     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
   354     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   355   in (plain_name_tab, inclass_name_tab) end
   356 
   357 fun uniquify facts =
   358   Termtab.fold (cons o snd)
   359       (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts
   360             Termtab.empty) []
   361 
   362 fun struct_induct_rule_on th =
   363   case Logic.strip_horn (prop_of th) of
   364     (prems, @{const Trueprop}
   365             $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
   366     if not (is_TVar ind_T) andalso length prems > 1 andalso
   367        exists (exists_subterm (curry (op aconv) p)) prems andalso
   368        not (exists (exists_subterm (curry (op aconv) a)) prems) then
   369       SOME (p_name, ind_T)
   370     else
   371       NONE
   372   | _ => NONE
   373 
   374 val instantiate_induct_timeout = seconds 0.01
   375 
   376 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   377   let
   378     fun varify_noninducts (t as Free (s, T)) =
   379         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
   380       | varify_noninducts t = t
   381     val p_inst =
   382       concl_prop |> map_aterms varify_noninducts |> close_form
   383                  |> lambda (Free ind_x)
   384                  |> hackish_string_for_term ctxt
   385   in
   386     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
   387       stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
   388   end
   389 
   390 fun type_match thy (T1, T2) =
   391   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   392   handle Type.TYPE_MATCH => false
   393 
   394 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
   395   case struct_induct_rule_on th of
   396     SOME (p_name, ind_T) =>
   397     let val thy = Proof_Context.theory_of ctxt in
   398       stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
   399               |> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout
   400                      (instantiate_induct_rule ctxt stmt p_name ax)))
   401     end
   402   | NONE => [ax]
   403 
   404 fun external_frees t =
   405   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   406 
   407 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   408   if Config.get ctxt instantiate_inducts then
   409     let
   410       val thy = Proof_Context.theory_of ctxt
   411       val ind_stmt =
   412         (hyp_ts |> filter_out (null o external_frees), concl_t)
   413         |> Logic.list_implies |> Object_Logic.atomize_term thy
   414       val ind_stmt_xs = external_frees ind_stmt
   415     in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
   416   else
   417     I
   418 
   419 fun maybe_filter_no_atps ctxt =
   420   not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
   421 
   422 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   423   let
   424     val thy = Proof_Context.theory_of ctxt
   425     val global_facts = Global_Theory.facts_of thy
   426     val local_facts = Proof_Context.facts_of ctxt
   427     val named_locals = local_facts |> Facts.dest_static []
   428     val assms = Assumption.all_assms_of ctxt
   429     fun is_good_unnamed_local th =
   430       not (Thm.has_name_hint th) andalso
   431       forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   432     val unnamed_locals =
   433       union Thm.eq_thm_prop (Facts.props local_facts) chained
   434       |> filter is_good_unnamed_local |> map (pair "" o single)
   435     val full_space =
   436       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   437     fun add_facts global foldx facts =
   438       foldx (fn (name0, ths) =>
   439         if name0 <> "" andalso
   440            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   441            (Facts.is_concealed facts name0 orelse
   442             not (can (Proof_Context.get_thms ctxt) name0) orelse
   443             (not generous andalso
   444              is_blacklisted_or_something ctxt ho_atp name0)) then
   445           I
   446         else
   447           let
   448             val n = length ths
   449             val multi = n > 1
   450             fun check_thms a =
   451               case try (Proof_Context.get_thms ctxt) a of
   452                 NONE => false
   453               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   454           in
   455             pair n
   456             #> fold_rev (fn th => fn (j, accum) =>
   457                    (j - 1,
   458                     if not (member Thm.eq_thm_prop add_ths th) andalso
   459                        (is_likely_tautology_too_meta_or_too_technical th orelse
   460                         (not generous andalso
   461                          is_too_complex ho_atp (prop_of th))) then
   462                       accum
   463                     else
   464                       let
   465                         val new =
   466                           (((fn () =>
   467                                 if name0 = "" then
   468                                   backquote_thm ctxt th
   469                                 else
   470                                   [Facts.extern ctxt facts name0,
   471                                    Name_Space.extern ctxt full_space name0]
   472                                   |> distinct (op =)
   473                                   |> find_first check_thms
   474                                   |> the_default name0
   475                                   |> make_name reserved multi j),
   476                              stature_of_thm global assms chained css name0 th),
   477                            th)
   478                       in
   479                         accum |> (if multi then apsnd else apfst) (cons new)
   480                       end)) ths
   481             #> snd
   482           end)
   483   in
   484     (* The single-theorem names go before the multiple-theorem ones (e.g.,
   485        "xxx" vs. "xxx(3)"), so that single names are preferred when both are
   486        available. *)
   487     `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   488           |> add_facts true Facts.fold_static global_facts global_facts
   489           |> op @
   490   end
   491 
   492 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
   493                      concl_t =
   494   if only andalso null add then
   495     []
   496   else
   497     let
   498       val chained =
   499         chained
   500         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   501     in
   502       (if only then
   503          maps (map (fn ((name, stature), th) => ((K name, stature), th))
   504                o fact_from_ref ctxt reserved chained css) add
   505        else
   506          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
   507            all_facts ctxt false ho_atp reserved add chained css
   508            |> filter_out (member Thm.eq_thm_prop del o snd)
   509            |> maybe_filter_no_atps ctxt
   510            |> uniquify
   511          end)
   512       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   513     end
   514 
   515 end;