multi-functional value keyword

--- a/src/HOL/Library/Eval.thy	Sat Sep 15 19:27:41 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Sat Sep 15 19:27:42 2007 +0200
@@ -34,11 +34,14 @@
 end;
 *}
 
+instance "prop" :: typ_of
+  "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
+
 instance itself :: (typ_of) typ_of
   "typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
 
-instance "prop" :: typ_of
-  "typ_of T \<equiv> STR ''prop'' {\<struct>} []" ..
+instance set :: (typ_of) typ_of
+  "typ_of T \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" ..
 
 instance int :: typ_of
   "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
@@ -153,7 +156,7 @@
 ML {*
 signature EVAL =
 sig
-  val eval_ref: term option ref
+  val eval_ref: (unit -> term) option ref
   val eval_conv: cterm -> thm
   val eval_print: (cterm -> thm) -> Proof.context -> term -> unit
   val eval_print_cmd: (cterm -> thm) -> string -> Toplevel.state -> unit
@@ -162,7 +165,7 @@
 structure Eval =
 struct
 
-val eval_ref = ref (NONE : term option);
+val eval_ref = ref (NONE : (unit -> term) option);
 
 end;
 *}
@@ -223,9 +226,11 @@
 ML {*
 val valueP =
   OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
-    ((OuterParse.opt_keyword "overloaded" -- OuterParse.term)
-      >> (fn (b, t) => Toplevel.no_timing o Toplevel.keep
-           (Eval.eval_print_cmd (if b then Eval.eval_conv else Codegen.evaluation_conv) t)));
+    (OuterParse.term
+      >> (fn t => Toplevel.no_timing o Toplevel.keep
+           (Eval.eval_print_cmd (fn ct => case try Eval.eval_conv ct
+     of SOME thm => thm
+      | NONE => Codegen.evaluation_conv ct) t)));
 
 val _ = OuterSyntax.add_parsers [valueP];
 *}

--- a/src/HOL/ex/Eval_Examples.thy	Sat Sep 15 19:27:41 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Sat Sep 15 19:27:42 2007 +0200
@@ -26,13 +26,14 @@
 
 text {* term evaluation *}
 
-value (overloaded) "(Suc 2 + 1) * 4"
-value (overloaded) "(Suc 2 + 1) * 4"
-value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
-value (overloaded) "nat 100"
-value (overloaded) "(10\<Colon>int) \<le> 12"
-value (overloaded) "[]::nat list"
-value (overloaded) "[(nat 100, ())]"
+value "(Suc 2 + 1) * 4"
+value "(Suc 2 + 1) * 4"
+value "(Suc 2 + Suc 0) * Suc 3"
+value "nat 100"
+value "(10\<Colon>int) \<le> 12"
+value "[]::nat list"
+value "[(nat 100, ())]"
+value "max (2::int) 4"
 
 text {* a fancy datatype *}
 
@@ -43,6 +44,6 @@
 and ('a, 'b) cair =
     Cair 'a 'b
 
-value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
+value "Shift (Cair (4::nat) [Suc 0])"
 
 end