--- a/src/HOL/Option.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Option.ML Wed Dec 24 10:02:30 1997 +0100
@@ -8,7 +8,7 @@
open Option;
qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
- (K [option.induct_tac "x" 1, Auto_tac()]);
+ (K [option.induct_tac "x" 1, Auto_tac]);
section "case analysis in premises";
@@ -31,7 +31,7 @@
res_inst_tac [("opt","x")] optionE 1,
forward_tac prems 1,
forward_tac prems 3,
- Auto_tac()]);
+ Auto_tac]);
fun option_case_tac i = EVERY [
etac option_caseE i,
hyp_subst_tac (i+1),
@@ -56,4 +56,4 @@
val option_map_SomeD = prove_goalw thy [option_map_def]
"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
optionE_tac "x" 1,
- Auto_tac()]);
+ Auto_tac]);