# 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