equal
deleted
inserted
replaced
337 local |
337 local |
338 |
338 |
339 fun dest_all ct = |
339 fun dest_all ct = |
340 (case Thm.term_of ct of |
340 (case Thm.term_of ct of |
341 Const ("Pure.all", _) $ Abs (a, _, _) => |
341 Const ("Pure.all", _) $ Abs (a, _, _) => |
342 let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct) |
342 let val (x, ct') = Thm.dest_abs (Thm.dest_arg ct) |
343 in SOME ((a, Thm.ctyp_of_cterm x), ct') end |
343 in SOME ((a, Thm.ctyp_of_cterm x), ct') end |
344 | _ => NONE); |
344 | _ => NONE); |
345 |
345 |
346 fun dest_all_list ct = |
346 fun dest_all_list ct = |
347 (case dest_all ct of |
347 (case dest_all ct of |