equal
deleted
inserted
replaced
535 else |
535 else |
536 NONE) |
536 NONE) |
537 Lambda_Lifting.is_quantifier |
537 Lambda_Lifting.is_quantifier |
538 #> fst |
538 #> fst |
539 |
539 |
540 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (s, T, t)) = |
540 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) = |
541 intentionalize_def t |
541 intentionalize_def t |
542 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
542 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) = |
543 let |
543 let |
544 fun lam T t = Abs (Name.uu, T, t) |
544 fun lam T t = Abs (Name.uu, T, t) |
545 val (head, args) = strip_comb t ||> rev |
545 val (head, args) = strip_comb t ||> rev |