src/HOL/HOL.thy
changeset 44021 7c39c83002b9
parent 43654 3f1a44c2d645
child 44121 44adaa6db327
     1.1 --- a/src/HOL/HOL.thy	Wed Aug 03 11:09:12 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Aug 03 13:59:59 2011 +0200
     1.3 @@ -1962,10 +1962,6 @@
     1.4  
     1.5  subsubsection {* Evaluation and normalization by evaluation *}
     1.6  
     1.7 -setup {*
     1.8 -  Value.add_evaluator ("SML", Codegen.eval_term)
     1.9 -*}
    1.10 -
    1.11  ML {*
    1.12  fun gen_eval_method conv ctxt = SIMPLE_METHOD'
    1.13    (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt)