# HG changeset patch
# User haftmann
# Date 1226588376 -3600
# Node ID eda4a5f64f2e36b34b73da491a6e2e5a3d5f0f28
# Parent  07073b1087ddc56990e970f3f0a23c0d45ddbce4
dropped superfluos eval_conv

diff -r 07073b1087dd -r eda4a5f64f2e src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Thu Nov 13 15:59:33 2008 +0100
+++ b/src/Tools/code/code_ml.ML	Thu Nov 13 15:59:36 2008 +0100
@@ -7,8 +7,6 @@
 
 signature CODE_ML =
 sig
-  val eval_conv: string * (unit -> thm) option ref
-    -> theory -> cterm -> string list -> thm
   val eval_term: string * (unit -> 'a) option ref
     -> theory -> term -> string list -> 'a
   val setup: theory -> theory
@@ -905,7 +903,6 @@
       in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
   in eval'' thy (rpair eval') ct end;
 
-fun eval_conv reff = eval Code_Thingol.eval_conv Thm.term_of reff;
 fun eval_term reff = eval Code_Thingol.eval_term I reff;