# HG changeset patch
# User wenzelm
# Date 1154000590 -7200
# Node ID 31998a8c7f2512536937294f238c3d09dacea7ff
# Parent  dcdd565a7fbe21afc701ba8979d685d2ed6ae039
removed obsolete is_fact (cf. Thm.no_prems);

diff -r dcdd565a7fbe -r 31998a8c7f25 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Jul 27 13:43:09 2006 +0200
+++ b/src/Pure/tactic.ML	Thu Jul 27 13:43:10 2006 +0200
@@ -59,7 +59,6 @@
   val delete_tagged_brl : (bool * thm) *
     (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
       ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
-  val is_fact           : thm -> bool
   val lessb             : (bool * thm) * (bool * thm) -> bool
   val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
   val make_elim         : thm -> thm
@@ -373,18 +372,13 @@
   while subgoal i+1,... are the premises of the rule.*)
 fun metacut_tac rule = bires_cut_tac [(false,rule)];
 
-(*Recognizes theorems that are not rules, but simple propositions*)
-fun is_fact rl =
-    case prems_of rl of
-        [] => true  |  _::_ => false;
-
 (*"Cut" a list of rules into the goal.  Their premises will become new
   subgoals.*)
 fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
 
 (*As above, but inserts only facts (unconditional theorems);
   generates no additional subgoals. *)
-fun cut_facts_tac ths = cut_rules_tac  (List.filter is_fact ths);
+fun cut_facts_tac ths = cut_rules_tac (filter Thm.no_prems ths);
 
 (*Introduce the given proposition as a lemma and subgoal*)
 fun subgoal_tac sprop =