# HG changeset patch
# User berghofe
# Date 1107364783 -3600
# Node ID d136af442665108feb1bfdd1f18b777eb27219b7
# Parent  7c638a46dcbbcd7d99ee1ade7cf9d88a54baa846
Replaced application of subst by simplesubst in proof of rev_induct
to avoid problems with program extraction.

diff -r 7c638a46dcbb -r d136af442665 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 02 18:06:25 2005 +0100
+++ b/src/HOL/List.thy	Wed Feb 02 18:19:43 2005 +0100
@@ -582,7 +582,7 @@
 
 lemma rev_induct [case_names Nil snoc]:
   "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
-apply(subst rev_rev_ident[symmetric])
+apply(simplesubst rev_rev_ident[symmetric])
 apply(rule_tac list = "rev xs" in list.induct, simp_all)
 done