--- a/src/HOL/Option.thy Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Option.thy Mon Mar 03 12:48:20 2014 +0100
@@ -28,7 +28,6 @@
setup {* Sign.mandatory_path "option" *}
lemmas inducts = option.induct
-lemmas recs = option.rec
lemmas cases = option.case
setup {* Sign.parent_path *}