src/HOL/Option.ML
changeset 4071 4747aefbbc52
parent 4032 4b1c69d8b767
child 4133 0a08c2b9b1ed
--- a/src/HOL/Option.ML	Mon Nov 03 08:16:35 1997 +0100
+++ b/src/HOL/Option.ML	Mon Nov 03 09:57:35 1997 +0100
@@ -5,5 +5,3 @@
 
 Derived rules
 *)
-
-val expand_option_case = split_option_case;