# HG changeset patch
# User nipkow
# Date 832328687 -7200
# Node ID f20c9abe4b50b264c0932f829eeea03dfcd41332
# Parent  f0c6aabc6c027efb6518419bcc4b1a550e052a35
Had to rename params because variable names in an induction rule changed.

diff -r f0c6aabc6c02 -r f20c9abe4b50 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Fri May 17 12:23:44 1996 +0200
+++ b/src/HOL/IMP/Hoare.ML	Fri May 17 12:24:47 1996 +0200
@@ -19,8 +19,10 @@
 by (rtac impI 1);
 by (etac induct2 1);
  br Gamma_mono 1;
+by(prune_params_tac);
+by(rename_tac "s t" 1);
 by (rewtac Gamma_def);  
-by(eres_inst_tac [("x","a")] allE 1);
+by(eres_inst_tac [("x","s")] allE 1);
 by (safe_tac comp_cs);
   by(ALLGOALS Asm_full_simp_tac);
 qed "hoare_sound";