equal
deleted
inserted
replaced
258 let |
258 let |
259 fun err msg = raise TERM (msg, [tm]); |
259 fun err msg = raise TERM (msg, [tm]); |
260 |
260 |
261 val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm) |
261 val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm) |
262 handle TERM _ => err "Not a meta-equality (==)"; |
262 handle TERM _ => err "Not a meta-equality (==)"; |
263 val (head, args) = Term.strip_comb lhs; |
263 val (head, args) = Term.strip_comb (Pattern.beta_eta_contract lhs); |
264 val (c, T) = Term.dest_Const head |
264 val (c, T) = Term.dest_Const head |
265 handle TERM _ => err "Head of lhs not a constant"; |
265 handle TERM _ => err "Head of lhs not a constant"; |
266 |
266 |
267 fun dest_free (Free (x, _)) = x |
267 fun dest_free (Free (x, _)) = x |
268 | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x |
268 | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x |