3972 @{code Eq} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q)) |
3972 @{code Eq} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q)) |
3973 | fm_of_term fs ps \<^Const_>\<open>less _ for p q\<close> = |
3973 | fm_of_term fs ps \<^Const_>\<open>less _ for p q\<close> = |
3974 @{code Lt} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q)) |
3974 @{code Lt} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q)) |
3975 | fm_of_term fs ps \<^Const_>\<open>less_eq _ for p q\<close> = |
3975 | fm_of_term fs ps \<^Const_>\<open>less_eq _ for p q\<close> = |
3976 @{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q)) |
3976 @{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q)) |
3977 | fm_of_term fs ps (\<^Const_>\<open>Ex _\<close> $ Abs (abs as (_, xT, _))) = |
3977 | fm_of_term fs ps \<^Const_>\<open>Ex _ for \<open>p as Abs _\<close>\<close> = |
3978 let val (xn', p') = Term.dest_abs abs |
3978 let val (x', p') = Term.dest_abs_global p |
3979 in @{code E} (fm_of_term (Free (xn', xT) :: fs) ps p') end |
3979 in @{code E} (fm_of_term (Free x' :: fs) ps p') end |
3980 | fm_of_term fs ps (\<^Const_>\<open>All _\<close> $ Abs (abs as (_, xT, _))) = |
3980 | fm_of_term fs ps \<^Const_>\<open>All _ for \<open>p as Abs _\<close>\<close> = |
3981 let val (xn', p') = Term.dest_abs abs |
3981 let val (x', p') = Term.dest_abs_global p |
3982 in @{code A} (fm_of_term (Free (xn', xT) :: fs) ps p') end |
3982 in @{code A} (fm_of_term (Free x' :: fs) ps p') end |
3983 | fm_of_term fs ps _ = error "fm_of_term"; |
3983 | fm_of_term fs ps _ = error "fm_of_term"; |
3984 |
3984 |
3985 fun term_of_num T ps (@{code poly.C} (a, b)) = |
3985 fun term_of_num T ps (@{code poly.C} (a, b)) = |
3986 let |
3986 let |
3987 val (c, d) = apply2 (@{code integer_of_int}) (a, b) |
3987 val (c, d) = apply2 (@{code integer_of_int}) (a, b) |