fixing the cut_tac method to work when there are no instantiations and the
supplied theorems have premises

--- a/src/Pure/Isar/method.ML	Tue Oct 15 15:37:57 2002 +0200
+++ b/src/Pure/Isar/method.ML	Thu Oct 17 10:52:59 2002 +0200
@@ -337,7 +337,7 @@
 val eres_inst = gen_res_inst Tactic.eres_inst_tac Tactic.eresolve_tac;
 val dres_inst = gen_res_inst Tactic.dres_inst_tac Tactic.dresolve_tac;
 val forw_inst = gen_res_inst Tactic.forw_inst_tac Tactic.forward_tac;
-val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_facts_tac;
+val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_rules_tac;
 
 
 (* simple Prolog interpreter *)

--- a/src/Pure/drule.ML	Tue Oct 15 15:37:57 2002 +0200
+++ b/src/Pure/drule.ML	Thu Oct 17 10:52:59 2002 +0200
@@ -501,7 +501,10 @@
 
 (** theorem equality **)
 
+(*True if the two theorems have the same signature.*)
 val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
+
+(*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
 val eq_thm_prop = op aconv o pairself Thm.prop_of;
 
 (*Useful "distance" function for BEST_FIRST*)

--- a/src/Pure/tactic.ML	Tue Oct 15 15:37:57 2002 +0200
+++ b/src/Pure/tactic.ML	Thu Oct 17 10:52:59 2002 +0200
@@ -29,6 +29,7 @@
                           int -> tactic
   val compose_tac       : (bool * thm * int) -> int -> tactic
   val cut_facts_tac     : thm list -> int -> tactic
+  val cut_rules_tac     : thm list -> int -> tactic
   val cut_inst_tac      : (string*string)list -> thm -> int -> tactic
   val datac             : thm -> int -> int -> tactic
   val defer_tac         : int -> tactic
@@ -346,9 +347,13 @@
     case prems_of rl of
         [] => true  |  _::_ => false;
 
-(*"Cut" all facts from theorem list into the goal as assumptions. *)
-fun cut_facts_tac ths i =
-    EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
+(*"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  (filter is_fact ths);
 
 (*Introduce the given proposition as a lemma and subgoal*)
 fun subgoal_tac sprop =

--- a/src/Pure/tctical.ML	Tue Oct 15 15:37:57 2002 +0200
+++ b/src/Pure/tctical.ML	Thu Oct 17 10:52:59 2002 +0200
@@ -291,10 +291,13 @@
 
 fun FILTER pred tac st = Seq.filter pred (tac st);
 
+(*Accept only next states that change the theorem somehow*)
 fun CHANGED tac st =
   let fun diff st' = not (Thm.eq_thm (st, st'));
   in Seq.filter diff (tac st) end;
 
+(*Accept only next states that change the theorem's prop field
+  (changes to signature, hyps, etc. don't count)*)
 fun CHANGED_PROP tac st =
   let fun diff st' = not (Drule.eq_thm_prop (st, st'));
   in Seq.filter diff (tac st) end;