# HG changeset patch
# User haftmann
# Date 1514839326 0
# Node ID 5ca7bb565ea29042082bb11d7fa472595891d595
# Parent  89be5a4f514b5829758b7e243f6027b63b238065
more correct name resolving

diff -r 89be5a4f514b -r 5ca7bb565ea2 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Mon Jan 01 20:42:05 2018 +0000
+++ b/src/Tools/Code/code_runtime.ML	Mon Jan 01 20:42:06 2018 +0000
@@ -469,15 +469,15 @@
       Code_Target.compilation_text' ctxt target some_module_name program''
         (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals;
         (*FIXME constrain signature*)
+    fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of
+          NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
+            "\nhas a user-defined serialization")
+        | SOME c' => c';
     fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of
           NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^
             "\nhas a user-defined serialization")
         | SOME c' => c';
-    fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of
-          NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
-            "\nhas a user-defined serialization")
-        | SOME c' => c';
-    val tyco_names =  map deresolve_const named_tycos;
+    val tyco_names =  map deresolve_tyco named_tycos;
     val const_names = map deresolve_const named_consts;
     val generated_code = space_implode "\n\n" (map snd ml_modules);
     val (of_term_code, of_term_names) =