# HG changeset patch
# User haftmann
# Date 1158842670 -7200
# Node ID 8c4d80e8025f7f615a3fb0f3c9760dd984bc65b0
# Parent  d80502f0d7018ca9f46c9056c16061583670bdfa
circumvented defect in SML/NJ type inference

diff -r d80502f0d701 -r 8c4d80e8025f src/HOL/ex/CodeEval.thy
--- a/src/HOL/ex/CodeEval.thy	Thu Sep 21 12:22:05 2006 +0200
+++ b/src/HOL/ex/CodeEval.thy	Thu Sep 21 14:44:30 2006 +0200
@@ -125,7 +125,7 @@
 structure Eval : EVAL =
 struct
 
-val eval_ref = ref NONE;
+val eval_ref = ref (NONE : term option);
 
 fun eval_term thy t =
   CodegenPackage.eval_term