# HG changeset patch
# User wenzelm
# Date 1006904291 -3600
# Node ID 3c3f98b3d9e70672ee6ccf8040bdedabfe673eac
# Parent  8df202daf55d56d0365aeda607d25276216cb641
join_rules RuleCases.save;

diff -r 8df202daf55d -r 3c3f98b3d9e7 src/Provers/induct_method.ML
--- 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;