equal
deleted
inserted
replaced
704 error "Cannot replay Metis proof in Isabelle without \ |
704 error "Cannot replay Metis proof in Isabelle without \ |
705 \\"Hilbert_Choice\"." |
705 \\"Hilbert_Choice\"." |
706 val ax_counts = |
706 val ax_counts = |
707 Int_Tysubst_Table.empty |
707 Int_Tysubst_Table.empty |
708 |> fold (fn (ax_no, (_, (tysubst, _))) => |
708 |> fold (fn (ax_no, (_, (tysubst, _))) => |
709 Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) |
709 Int_Tysubst_Table.map_default ((ax_no, [](*###*)), 0) |
710 (Integer.add 1)) substs |
710 (Integer.add 1)) substs |
711 |> Int_Tysubst_Table.dest |
711 |> Int_Tysubst_Table.dest |
712 val needed_axiom_props = |
712 val needed_axiom_props = |
713 0 upto length axioms - 1 ~~ axioms |
713 0 upto length axioms - 1 ~~ axioms |
714 |> map_filter (fn (_, NONE) => NONE |
714 |> map_filter (fn (_, NONE) => NONE |