corrected bind_thm: now applies "standard" uniformly.

--- a/src/Pure/Thy/thy_read.ML	Mon Aug 07 16:37:47 1995 +0200
+++ b/src/Pure/Thy/thy_read.ML	Tue Aug 08 09:27:02 1995 +0200
@@ -521,9 +521,8 @@
 val qed_thm = ref flexpair_def(*dummy*);
 
 fun bind_thm (name, thm) =
-  (qed_thm := thm;
-   use_string ["val " ^ name ^ " = standard (store_thm (" ^ quote name ^
-               ", !qed_thm));"]);
+  (qed_thm := standard thm;
+   use_string ["val " ^name^ " = store_thm (" ^quote name^", !qed_thm);"]);
 
 fun qed name =
   use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ ", result ());"];