228 | simp_not_not t = t |
228 | simp_not_not t = t |
229 |
229 |
230 (* Match untyped terms. *) |
230 (* Match untyped terms. *) |
231 fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b) |
231 fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b) |
232 | untyped_aconv (Free (a, _), Free (b, _)) = (a = b) |
232 | untyped_aconv (Free (a, _), Free (b, _)) = (a = b) |
233 | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = (a = b) |
233 | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = |
|
234 (a = b) (* ignore variable numbers *) |
234 | untyped_aconv (Bound i, Bound j) = (i = j) |
235 | untyped_aconv (Bound i, Bound j) = (i = j) |
235 | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u) |
236 | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u) |
236 | untyped_aconv (t1 $ t2, u1 $ u2) = |
237 | untyped_aconv (t1 $ t2, u1 $ u2) = |
237 untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2) |
238 untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2) |
238 | untyped_aconv _ = false |
239 | untyped_aconv _ = false |