# HG changeset patch
# User haftmann
# Date 1191873808 -7200
# Node ID dc56dd1b3cdabe24518d9ac79d2f9b908e72d0bd
# Parent  fc90277c0dd7b946b912fa35c4ffa7826d08035c
simplified evaluation

diff -r fc90277c0dd7 -r dc56dd1b3cda src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Mon Oct 08 22:03:25 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Mon Oct 08 22:03:28 2007 +0200
@@ -169,7 +169,7 @@
 val eval_ref = ref (NONE : (unit -> term) option);
 
 fun eval_invoke thy code ((_, ty), t) deps _ =
-  CodePackage.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
+  CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
 
 fun eval_term thy =
   TermOf.mk_term_of
diff -r fc90277c0dd7 -r dc56dd1b3cda src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Mon Oct 08 22:03:25 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Mon Oct 08 22:03:28 2007 +0200
@@ -52,7 +52,7 @@
 value ("normal_form") "max (2::int) 4"
 
 value "of_int 2 / of_int 4 * (1::rat)"
-(*value (code) "of_int 2 / of_int 4 * (1::rat)" FIXME*)
+(*value (code) "of_int 2 / of_int 4 * (1::rat)"*)
 value (SML) "of_int 2 / of_int 4 * (1::rat)"
 value ("normal_form") "of_int 2 / of_int 4 * (1::rat)"
 
diff -r fc90277c0dd7 -r dc56dd1b3cda src/Tools/code/code_name.ML
--- a/src/Tools/code/code_name.ML	Mon Oct 08 22:03:25 2007 +0200
+++ b/src/Tools/code/code_name.ML	Mon Oct 08 22:03:28 2007 +0200
@@ -27,6 +27,7 @@
   val instance_rev: theory -> string -> (class * string) option
   val const: theory -> string -> string
   val const_rev: theory -> string -> string option
+  val value_name: string
   val labelled_name: theory -> string -> string
 
   val setup: theory -> theory
@@ -405,7 +406,9 @@
 
 in
 
-fun labelled_name thy suffix_name =
+val value_name = "Isabelle_Eval.EVAL.EVAL"
+
+fun labelled_name thy suffix_name = if suffix_name = value_name then "<term>" else
   let
     val category = category_of suffix_name;
     val name = NameSpace.qualifier suffix_name;