# HG changeset patch
# User bulwahn
# Date 1312372799 -7200
# Node ID 7c39c83002b96ff9fd29c353bdd986fb8329f0b3
# Parent  376c1e7b320cf1cca12f3f0b6494a91380012407
removing the SML evaluator

diff -r 376c1e7b320c -r 7c39c83002b9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 03 11:09:12 2011 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 03 13:59:59 2011 +0200
@@ -1962,10 +1962,6 @@
 
 subsubsection {* Evaluation and normalization by evaluation *}
 
-setup {*
-  Value.add_evaluator ("SML", Codegen.eval_term)
-*}
-
 ML {*
 fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt)