src/Doc/Tutorial/Recdef/simplification.thy

--- a/src/Doc/Tutorial/Recdef/simplification.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Recdef/simplification.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -40,7 +40,7 @@
 different ways.
 
 The most radical solution is to disable the offending theorem
-@{thm[source]split_if},
+@{thm[source]if_split},
 as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
 approach: you will often have to invoke the rule explicitly when
 @{text "if"} is involved.