# HG changeset patch
# User wenzelm
# Date 1140991308 -3600
# Node ID 99a72b8c997440ce4444bd5f7d70c18bdc8d95b0
# Parent  22893b10e2d0023f5533ad4e3a5bc87c19fe49f9
rewrite_goals_rule_aux: actually use prems if present;

diff -r 22893b10e2d0 -r 99a72b8c9974 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Sun Feb 26 23:01:47 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Sun Feb 26 23:01:48 2006 +0100
@@ -1190,10 +1190,9 @@
 fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
 
 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
-fun rewrite_goals_rule_aux _ []   th = th
-  | rewrite_goals_rule_aux prover thms th =
-      Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, false) prover
-        (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
+fun rewrite_goals_rule_aux prover thms th =
+  Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) prover
+    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
 
 (*Rewrite the subgoal of a proof state (represented by a theorem)*)
 fun rewrite_goal_rule mode prover ss i thm =