author | wenzelm |
Sat, 04 Sep 1999 20:59:33 +0200 | |
changeset 7467 | 71e5d8671e7b |
parent 7466 | 7df66ce6508a |
child 7468 | 6ce03d2f7d91 |
src/Pure/drule.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/drule.ML Sat Sep 04 20:57:32 1999 +0200 +++ b/src/Pure/drule.ML Sat Sep 04 20:59:33 1999 +0200 @@ -521,7 +521,7 @@ def in equal_elim def' th end - handle THM _ => err th | bind => err th + handle THM _ => err th | Bind => err th in val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) and flexpair_elim = flexpair_inst ProtoPure.flexpair_def