# HG changeset patch
# User nipkow
# Date 807866822 -7200
# Node ID 53e4b22aa1f28ca6ccb2c33c3ecfffd68020256f
# Parent  d99d13a0213fe1a38f197a343e52638bd37d6331
corrected bind_thm: now applies "standard" uniformly.

diff -r d99d13a0213f -r 53e4b22aa1f2 src/Pure/Thy/thy_read.ML
--- 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 ());"];