removed obsolete is_fact (cf. Thm.no_prems);
authorwenzelm
Thu Jul 27 13:43:10 2006 +0200 (2006-07-27)
changeset 2023231998a8c7f25
parent 20231 dcdd565a7fbe
child 20233 ece639738db3
removed obsolete is_fact (cf. Thm.no_prems);
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Jul 27 13:43:09 2006 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Jul 27 13:43:10 2006 +0200
     1.3 @@ -59,7 +59,6 @@
     1.4    val delete_tagged_brl : (bool * thm) *
     1.5      (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
     1.6        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
     1.7 -  val is_fact           : thm -> bool
     1.8    val lessb             : (bool * thm) * (bool * thm) -> bool
     1.9    val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
    1.10    val make_elim         : thm -> thm
    1.11 @@ -373,18 +372,13 @@
    1.12    while subgoal i+1,... are the premises of the rule.*)
    1.13  fun metacut_tac rule = bires_cut_tac [(false,rule)];
    1.14  
    1.15 -(*Recognizes theorems that are not rules, but simple propositions*)
    1.16 -fun is_fact rl =
    1.17 -    case prems_of rl of
    1.18 -        [] => true  |  _::_ => false;
    1.19 -
    1.20  (*"Cut" a list of rules into the goal.  Their premises will become new
    1.21    subgoals.*)
    1.22  fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
    1.23  
    1.24  (*As above, but inserts only facts (unconditional theorems);
    1.25    generates no additional subgoals. *)
    1.26 -fun cut_facts_tac ths = cut_rules_tac  (List.filter is_fact ths);
    1.27 +fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths);
    1.28  
    1.29  (*Introduce the given proposition as a lemma and subgoal*)
    1.30  fun subgoal_tac sprop =