equal
deleted
inserted
replaced
41 local |
41 local |
42 fun instances_from_net match f net ct = |
42 fun instances_from_net match f net ct = |
43 let |
43 let |
44 val lookup = if match then Net.match_term else Net.unify_term |
44 val lookup = if match then Net.match_term else Net.unify_term |
45 val xthms = lookup net (Thm.term_of ct) |
45 val xthms = lookup net (Thm.term_of ct) |
46 fun select ct = map_filter (f (maybe_instantiate ct)) xthms |
46 fun select ct = map_filter (f (maybe_instantiate ct)) xthms |
47 fun select' ct = |
47 fun select' ct = |
48 let val thm = Thm.trivial ct |
48 let val thm = Thm.trivial ct |
49 in map_filter (f (try (fn rule => rule COMP thm))) xthms end |
49 in map_filter (f (try (fn rule => rule COMP thm))) xthms end |
50 in (case select ct of [] => select' ct | xthms' => xthms') end |
50 in (case select ct of [] => select' ct | xthms' => xthms') end |
51 in |
51 in |