--- a/src/HOL/Wellfounded_Relations.ML Mon Mar 17 17:37:48 2003 +0100
+++ b/src/HOL/Wellfounded_Relations.ML Mon Mar 17 18:38:50 2003 +0100
@@ -43,6 +43,7 @@
by (mp_tac 1);
by (Blast_tac 1);
qed "wf_inv_image";
+Addsimps [wf_inv_image];
AddSIs [wf_inv_image];