circumvented defect in SML/NJ type inference
authorhaftmann
Thu Sep 21 14:44:30 2006 +0200 (2006-09-21)
changeset 206558c4d80e8025f
parent 20654 d80502f0d701
child 20656 9de0a076b3fc
circumvented defect in SML/NJ type inference
src/HOL/ex/CodeEval.thy
     1.1 --- a/src/HOL/ex/CodeEval.thy	Thu Sep 21 12:22:05 2006 +0200
     1.2 +++ b/src/HOL/ex/CodeEval.thy	Thu Sep 21 14:44:30 2006 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4  structure Eval : EVAL =
     1.5  struct
     1.6  
     1.7 -val eval_ref = ref NONE;
     1.8 +val eval_ref = ref (NONE : term option);
     1.9  
    1.10  fun eval_term thy t =
    1.11    CodegenPackage.eval_term