src/Tools/Code/code_runtime.ML
changeset 39537 41afe7124aa6
parent 39485 f7270a5e2550
child 39605 6dc866b9c548
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sun Sep 19 11:33:39 2010 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Sep 20 08:53:37 2010 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
     1.5    (the_default target some_target) NONE "Code" [];
     1.6  
     1.7 -fun base_evaluator cookie serializer naming thy program ((vs, ty), t) deps args =
     1.8 +fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args =
     1.9    let
    1.10      val ctxt = ProofContext.init_global thy;
    1.11      val _ = if Code_Thingol.contains_dictvar t then