src/HOL/Code_Evaluation.thy
changeset 35299 4f4d5bf4ea08
parent 34028 1e6206763036
child 35366 6d474096698c
equal deleted inserted replaced
35279:4f6760122b2a 35299:4f4d5bf4ea08
    74     let
    74     let
    75       val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    75       val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
    76         andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    76         andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    77     in if need_inst then add_term_of tyco raw_vs thy else thy end;
    77     in if need_inst then add_term_of tyco raw_vs thy else thy end;
    78 in
    78 in
    79   Code.type_interpretation ensure_term_of
    79   Code.datatype_interpretation ensure_term_of
       
    80   #> Code.abstype_interpretation ensure_term_of
    80 end
    81 end
    81 *}
    82 *}
    82 
    83 
    83 setup {*
    84 setup {*
    84 let
    85 let
   112   fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
   113   fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
   113     let
   114     let
   114       val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   115       val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
   115     in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
   116     in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
   116 in
   117 in
   117   Code.type_interpretation ensure_term_of_code
   118   Code.datatype_interpretation ensure_term_of_code
   118 end
   119 end
   119 *}
   120 *}
   120 
   121 
   121 
   122 
   122 subsubsection {* Code generator setup *}
   123 subsubsection {* Code generator setup *}