join_rules RuleCases.save;

--- a/src/Provers/induct_method.ML	Wed Nov 28 00:37:40 2001 +0100
+++ b/src/Provers/induct_method.ML	Wed Nov 28 00:38:11 2001 +0100
@@ -182,7 +182,8 @@
           [foldr1 (fn (x, x') => [x, x'] MRS Data.conjI)
             (map (fn x => Drule.implies_elim_list x asms) (th :: ths))
           |> Drule.implies_intr_list cprems
-          |> Drule.standard']
+          |> Drule.standard'
+          |> RuleCases.save th]
         end;