src/Tools/Code/code_runtime.ML
changeset 42359 6ca5407863ed
parent 41944 b97091ae583a
child 42361 23f352990944
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -188,19 +188,23 @@
     1.4  
     1.5  fun evaluation_code thy module_name tycos consts =
     1.6    let
     1.7 +    val ctxt = ProofContext.init_global thy;
     1.8      val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
     1.9      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    1.10 -    val (ml_code, target_names) = Code_Target.produce_code_for thy
    1.11 -      target NONE module_name [] naming program (consts' @ tycos');
    1.12 +    val (ml_code, target_names) =
    1.13 +      Code_Target.produce_code_for thy
    1.14 +        target NONE module_name [] naming program (consts' @ tycos');
    1.15      val (consts'', tycos'') = chop (length consts') target_names;
    1.16 -    val consts_map = map2 (fn const => fn NONE =>
    1.17 -        error ("Constant " ^ (quote o Code.string_of_const thy) const
    1.18 -          ^ "\nhas a user-defined serialization")
    1.19 -      | SOME const'' => (const, const'')) consts consts''
    1.20 -    val tycos_map = map2 (fn tyco => fn NONE =>
    1.21 -        error ("Type " ^ (quote o Sign.extern_type thy) tyco
    1.22 -          ^ "\nhas a user-defined serialization")
    1.23 -      | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
    1.24 +    val consts_map = map2 (fn const =>
    1.25 +      fn NONE =>
    1.26 +          error ("Constant " ^ (quote o Code.string_of_const thy) const ^
    1.27 +            "\nhas a user-defined serialization")
    1.28 +       | SOME const'' => (const, const'')) consts consts''
    1.29 +    val tycos_map = map2 (fn tyco =>
    1.30 +      fn NONE =>
    1.31 +          error ("Type " ^ quote (ProofContext.extern_type ctxt tyco) ^
    1.32 +            "\nhas a user-defined serialization")
    1.33 +        | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
    1.34    in (ml_code, (tycos_map, consts_map)) end;
    1.35  
    1.36