more correct name resolving
authorhaftmann
Mon Jan 01 20:42:06 2018 +0000 (18 months ago)
changeset 673285ca7bb565ea2
parent 67327 89be5a4f514b
child 67329 eabcd2e2bc9b
more correct name resolving
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Mon Jan 01 20:42:05 2018 +0000
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Jan 01 20:42:06 2018 +0000
     1.3 @@ -469,15 +469,15 @@
     1.4        Code_Target.compilation_text' ctxt target some_module_name program''
     1.5          (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals;
     1.6          (*FIXME constrain signature*)
     1.7 +    fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of
     1.8 +          NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
     1.9 +            "\nhas a user-defined serialization")
    1.10 +        | SOME c' => c';
    1.11      fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of
    1.12            NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^
    1.13              "\nhas a user-defined serialization")
    1.14          | SOME c' => c';
    1.15 -    fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of
    1.16 -          NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
    1.17 -            "\nhas a user-defined serialization")
    1.18 -        | SOME c' => c';
    1.19 -    val tyco_names =  map deresolve_const named_tycos;
    1.20 +    val tyco_names =  map deresolve_tyco named_tycos;
    1.21      val const_names = map deresolve_const named_consts;
    1.22      val generated_code = space_implode "\n\n" (map snd ml_modules);
    1.23      val (of_term_code, of_term_names) =