equal
deleted
inserted
replaced
1336 thy |> Theory.defs_of |
1336 thy |> Theory.defs_of |
1337 |> Defs.all_specifications_of |
1337 |> Defs.all_specifications_of |
1338 |> maps snd |> map_filter #def |
1338 |> maps snd |> map_filter #def |
1339 |> Ord_List.make fast_string_ord |
1339 |> Ord_List.make fast_string_ord |
1340 in |
1340 in |
1341 Theory.nodes_of thy |
1341 Thm.all_axioms_of thy |
1342 |> maps Thm.axioms_of |
|
1343 |> map (apsnd (subst_atomic subst o Thm.prop_of)) |
1342 |> map (apsnd (subst_atomic subst o Thm.prop_of)) |
1344 |> sort (fast_string_ord o apply2 fst) |
1343 |> sort (fast_string_ord o apply2 fst) |
1345 |> Ord_List.inter (fast_string_ord o apsnd fst) def_names |
1344 |> Ord_List.inter (fast_string_ord o apsnd fst) def_names |
1346 |> map snd |
1345 |> map snd |
1347 end |
1346 end |