equal
deleted
inserted
replaced
193 let |
193 let |
194 val tuple = mk_tuples ts |
194 val tuple = mk_tuples ts |
195 val T = fastype_of tuple |
195 val T = fastype_of tuple |
196 in |
196 in |
197 \<^term>\<open>Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option\<close> $ |
197 \<^term>\<open>Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option\<close> $ |
198 (absdummy \<^typ>\<open>unit\<close> (@{const yxml_string_of_term} $ |
198 (absdummy \<^typ>\<open>unit\<close> (\<^const>\<open>yxml_string_of_term\<close> $ |
199 (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^typ>\<open>term\<close>) $ tuple))) |
199 (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^typ>\<open>term\<close>) $ tuple))) |
200 end |
200 end |
201 |
201 |
202 fun test_terms ctxt ts target = |
202 fun test_terms ctxt ts target = |
203 let |
203 let |