474 #> pair @{const True} |
474 #> pair @{const True} |
475 else |
475 else |
476 pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u) |
476 pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u) |
477 |
477 |
478 val combinator_table = |
478 val combinator_table = |
479 [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), |
479 [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), |
480 (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}), |
480 (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), |
481 (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}), |
481 (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), |
482 (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}), |
482 (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}), |
483 (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})] |
483 (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})] |
484 |
484 |
485 fun uncombine_term thy = |
485 fun uncombine_term thy = |
486 let |
486 let |
487 fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) |
487 fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) |
488 | aux (Abs (s, T, t')) = Abs (s, T, aux t') |
488 | aux (Abs (s, T, t')) = Abs (s, T, aux t') |