# HG changeset patch
# User clasohm
# Date 823778776 -3600
# Node ID 617ca7312ceb3e17757cbe39b6b6fcdd507978a9
# Parent  1a60df4fd63db719d4b8237a408cda1113384c1d
simplified bind_thm

diff -r 1a60df4fd63d -r 617ca7312ceb src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Wed Feb 07 13:36:56 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML	Thu Feb 08 12:26:16 1996 +0100
@@ -1062,7 +1062,7 @@
 
 fun bind_thm (name, thm) =
  (qed_thm := standard thm;
-  store_thm (name, standard thm);
+  store_thm (name, !qed_thm);
   use_string ["val " ^ name ^ " = !qed_thm;"]);
 
 fun qed name =