equal
deleted
inserted
replaced
1848 fun def_table_for get ctxt subst = |
1848 fun def_table_for get ctxt subst = |
1849 ctxt |> get |> map (pair_for_prop o subst_atomic subst) |
1849 ctxt |> get |> map (pair_for_prop o subst_atomic subst) |
1850 |> AList.group (op =) |> Symtab.make |
1850 |> AList.group (op =) |> Symtab.make |
1851 |
1851 |
1852 fun const_def_tables ctxt subst ts = |
1852 fun const_def_tables ctxt subst ts = |
1853 (def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst, |
1853 (def_table_for (map prop_of o Nitpick_Unfolds.get) ctxt subst, |
1854 fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) |
1854 fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) |
1855 (map pair_for_prop ts) Symtab.empty) |
1855 (map pair_for_prop ts) Symtab.empty) |
1856 |
1856 |
1857 fun paired_with_consts t = map (rpair t) (Term.add_const_names t []) |
1857 fun paired_with_consts t = map (rpair t) (Term.add_const_names t []) |
1858 fun const_nondef_table ts = |
1858 fun const_nondef_table ts = |