equal
deleted
inserted
replaced
219 fun dest_comb (f $ a) = (f, a) |
219 fun dest_comb (f $ a) = (f, a) |
220 fun dest_bcomb ((_ $ l) $ r) = (l, r) |
220 fun dest_bcomb ((_ $ l) $ r) = (l, r) |
221 |
221 |
222 fun unlam t = |
222 fun unlam t = |
223 (case t of |
223 (case t of |
224 Abs a => snd (Term.dest_abs a) |
224 Abs _ => snd (Term.dest_abs_global t) |
225 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))) |
225 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))) |
226 |
226 |
227 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
227 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
228 |
228 |
229 (* We apply apply_rsp only in case if the type needs lifting. |
229 (* We apply apply_rsp only in case if the type needs lifting. |