ex/MT.ML

--- a/ex/MT.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/ex/MT.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -536,7 +536,7 @@
 
 goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
 by infsys_mono_tac;
-val mono_hasty_fun = store_thm("mono_hasty_fun",  result());
+bind_thm("mono_hasty_fun",  result());
 
 (* 
   Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it