# HG changeset patch
# User berghofe
# Date 959702569 -7200
# Node ID 93af64f54bf2d6b1b469d6c8e3def8eaca776602
# Parent  c20d58286a51a4a787a7728e64336df2eb559438
the is now defined using primrec, avoiding explicit use of arbitrary.

diff -r c20d58286a51 -r 93af64f54bf2 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Tue May 30 16:08:38 2000 +0200
+++ b/src/HOL/Option.ML	Tue May 30 18:02:49 2000 +0200
@@ -42,16 +42,6 @@
 qed "option_caseE";
 
 
-section "the";
-
-Goalw [the_def] "the (Some x) = x";
-by (Simp_tac 1);
-qed "the_Some";
-
-Addsimps [the_Some];
-
-
-
 section "option_map";
 
 Goalw [option_map_def] "option_map f None = None";
diff -r c20d58286a51 -r 93af64f54bf2 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Tue May 30 16:08:38 2000 +0200
+++ b/src/HOL/Option.thy	Tue May 30 18:02:49 2000 +0200
@@ -10,21 +10,19 @@
 
 datatype 'a option = None | Some 'a
 
-constdefs
+consts
+  the :: "'a option => 'a"
+  o2s :: "'a option => 'a set"
 
-  the		:: "'a option => 'a"
- "the == %y. case y of None => arbitrary | Some x => x"
+primrec
+ "the (Some x) = x"
 
+primrec
+ "o2s  None    = {}"
+ "o2s (Some x) = {x}"
+
+constdefs
   option_map	:: "('a => 'b) => ('a option => 'b option)"
  "option_map == %f y. case y of None => None | Some x => Some (f x)"
 
-consts
-
-  o2s	   :: "'a option => 'a set"
-
-primrec
-
- "o2s  None    = {}"
- "o2s (Some x) = {x}"
-
 end