# HG changeset patch
# User haftmann
# Date 1291911943 -3600
# Node ID c1d1ec5b90f1944e402ff985249beb1c5db8d2ec
# Parent  6c0940392fb4271b2f416480a1e1e84144412f3b
tuned names

diff -r 6c0940392fb4 -r c1d1ec5b90f1 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Dec 09 17:25:43 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Dec 09 17:25:43 2010 +0100
@@ -92,7 +92,7 @@
 fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args =
   let
     val ctxt = ProofContext.init_global thy;
-    val _ = if Code_Thingol.contains_dictvar t then
+    val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
     val v' = Name.variant (map fst vs) "a";
     val vs' = (v', []) :: vs