IOA/meta_theory/Option.ML

--- a/IOA/meta_theory/Option.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/IOA/meta_theory/Option.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -13,4 +13,4 @@
  br (prem RS rev_mp) 1;
  by (Option.option.induct_tac "opt" 1);
  by (ALLGOALS(fast_tac HOL_cs));
-val optE = standard(result() RS disjE);
+val optE = store_thm("optE", standard(result() RS disjE));