equal
deleted
inserted
replaced
82 let fun atoms th = |
82 let fun atoms th = |
83 (case concl_of th of |
83 (case concl_of th of |
84 Const("Trueprop",_) $ p => |
84 Const("Trueprop",_) $ p => |
85 (case head_of p of |
85 (case head_of p of |
86 Const(a,_) => |
86 Const(a,_) => |
87 (case assoc(pairs,a) of |
87 (case AList.lookup (op =) pairs a of |
88 SOME(rls) => List.concat (map atoms ([th] RL rls)) |
88 SOME(rls) => List.concat (map atoms ([th] RL rls)) |
89 | NONE => [th]) |
89 | NONE => [th]) |
90 | _ => [th]) |
90 | _ => [th]) |
91 | _ => [th]) |
91 | _ => [th]) |
92 in atoms end; |
92 in atoms end; |