diff -r cc274e47f607 -r 93c093620c28 src/HOL/Option.ML --- a/src/HOL/Option.ML Mon Oct 07 10:26:00 1996 +0200 +++ b/src/HOL/Option.ML Mon Oct 07 10:28:44 1996 +0200 @@ -27,5 +27,4 @@ by (option.induct_tac "opt" 1); by (Simp_tac 1); by (Asm_full_simp_tac 1); -by (Fast_tac 1); qed"expand_option_case";