equal
deleted
inserted
replaced
107 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
107 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
108 [TermOf.class_term_of] ((K o K o pair) []) mk |
108 [TermOf.class_term_of] ((K o K o pair) []) mk |
109 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end |
109 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end |
110 *} |
110 *} |
111 |
111 |
|
112 text {* Disable for characters and ml_strings *} |
|
113 |
|
114 code_const "typ_of \<Colon> char itself \<Rightarrow> typ" and "term_of \<Colon> char \<Rightarrow> term" |
|
115 (SML "!((_); raise Fail \"typ'_of'_char\")" |
|
116 and "!((_); raise Fail \"term'_of'_char\")") |
|
117 (OCaml "!((_); failwith \"typ'_of'_char\")" |
|
118 and "!((_); failwith \"term'_of'_char\")") |
|
119 (Haskell "error/ \"typ'_of'_char\"" |
|
120 and "error/ \"term'_of'_char\"") |
|
121 |
|
122 code_const "term_of \<Colon> ml_string \<Rightarrow> term" |
|
123 (SML "!((_); raise Fail \"term'_of'_ml'_string\")") |
|
124 (OCaml "!((_); failwith \"term'_of'_ml'_string\")") |
112 |
125 |
113 subsection {* Evaluation infrastructure *} |
126 subsection {* Evaluation infrastructure *} |
114 |
127 |
115 ML {* |
128 ML {* |
116 signature EVAL = |
129 signature EVAL = |