--- 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 ());"];