src/Tools/Code/code_runtime.ML
changeset 55304 55ac31bc08a4
parent 55188 7ca0204ece66
child 55683 5732a55b9232
equal deleted inserted replaced
55303:35354009ca25 55304:55ac31bc08a4
   207           error ("Constant " ^ (quote o Code.string_of_const thy) const ^
   207           error ("Constant " ^ (quote o Code.string_of_const thy) const ^
   208             "\nhas a user-defined serialization")
   208             "\nhas a user-defined serialization")
   209        | SOME const' => (const, const')) consts consts'
   209        | SOME const' => (const, const')) consts consts'
   210     val tycos_map = map2 (fn tyco =>
   210     val tycos_map = map2 (fn tyco =>
   211       fn NONE =>
   211       fn NONE =>
   212           error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
   212           error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
   213             "\nhas a user-defined serialization")
   213             "\nhas a user-defined serialization")
   214         | SOME tyco' => (tyco, tyco')) tycos tycos';
   214         | SOME tyco' => (tyco, tyco')) tycos tycos';
   215   in (ml_code, (tycos_map, consts_map)) end;
   215   in (ml_code, (tycos_map, consts_map)) end;
   216 
   216 
   217 
   217