# HG changeset patch
# User paulson
# Date 905441527 -7200
# Node ID 7c5b2a8adbf0683598d3ada279314af722b1e662
# Parent  6376d5cbb6acd543d5de3e168a9ef4f4bfdc0f9c
a step to help a proof

diff -r 6376d5cbb6ac -r 7c5b2a8adbf0 src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Thu Sep 10 17:30:50 1998 +0200
+++ b/src/HOL/ex/Primrec.ML	Thu Sep 10 17:32:07 1998 +0200
@@ -201,6 +201,7 @@
 by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1);
 by Safe_tac;
 by (Asm_simp_tac 1);
+by (rtac exI 1);
 by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1);
 qed "COMP_map_lemma";