src/Tools/Code/code_runtime.ML
changeset 41101 c1d1ec5b90f1
parent 41099 5cf62cefbbb4
child 41184 5c6f44d22f51
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Dec 09 17:25:43 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Dec 09 17:25:43 2010 +0100
     1.3 @@ -92,7 +92,7 @@
     1.4  fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args =
     1.5    let
     1.6      val ctxt = ProofContext.init_global thy;
     1.7 -    val _ = if Code_Thingol.contains_dictvar t then
     1.8 +    val _ = if Code_Thingol.contains_dict_var t then
     1.9        error "Term to be evaluated contains free dictionaries" else ();
    1.10      val v' = Name.variant (map fst vs) "a";
    1.11      val vs' = (v', []) :: vs