diff -r 0fd3caa5d8b2 -r bca45be2d25b src/HOL/Datatype.ML
--- a/src/HOL/Datatype.ML	Thu Feb 21 20:06:39 2002 +0100
+++ b/src/HOL/Datatype.ML	Thu Feb 21 20:08:09 2002 +0100
@@ -62,34 +62,31 @@
   val size = thms "prod.size";
 end;
 
-
-(** sum_case -- the selection operator for sums **)
-
-(*compatibility*)
-val [sum_case_Inl, sum_case_Inr] = sum.cases;
-bind_thm ("sum_case_Inl", sum_case_Inl);
-bind_thm ("sum_case_Inr", sum_case_Inr);
-
-Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
-by (EVERY1 [res_inst_tac [("s","s")] sumE,
-            etac ssubst, rtac sum_case_Inl,
-            etac ssubst, rtac sum_case_Inr]);
-qed "surjective_sum";
+structure option =
+struct
+  val distinct = thms "option.distinct";
+  val inject = thms "option.inject";
+  val exhaust = thm "option.exhaust";
+  val cases = thms "option.cases";
+  val split = thm "option.split";
+  val split_asm = thm "option.split_asm";
+  val induct = thm "option.induct";
+  val recs = thms "option.recs";
+  val simps = thms "option.simps";
+  val size = thms "option.size";
+end;
 
-(*Prevents simplification of f and g: much faster*)
-Goal "s=t ==> sum_case f g s = sum_case f g t";
-by (etac arg_cong 1);
-qed "sum_case_weak_cong";
-
-val [p1,p2] = Goal
-  "[| sum_case f1 f2 = sum_case g1 g2;  \
-\     [| f1 = g1; f2 = g2 |] ==> P |] \
-\  ==> P";
-by (rtac p2 1);
-by (rtac ext 1);
-by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
-by (Asm_full_simp_tac 1);
-by (rtac ext 1);
-by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
-by (Asm_full_simp_tac 1);
-qed "sum_case_inject";
+val elem_o2s = thm "elem_o2s";
+val not_None_eq = thm "not_None_eq";
+val not_Some_eq = thm "not_Some_eq";
+val o2s_empty_eq = thm "o2s_empty_eq";
+val option_caseE = thm "option_caseE";
+val option_map_None = thm "option_map_None";
+val option_map_Some = thm "option_map_Some";
+val option_map_def = thm "option_map_def";
+val option_map_eq_Some = thm "option_map_eq_Some";
+val option_map_o_sum_case = thm "option_map_o_sum_case";
+val ospec = thm "ospec";
+val sum_case_inject = thm "sum_case_inject";
+val sum_case_weak_cong = thm "sum_case_weak_cong";
+val surjective_sum = thm "surjective_sum";