--- 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
--- 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)"
--- 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;