author | clasohm |
Thu, 08 Feb 1996 12:26:16 +0100 | |
changeset 1483 | 617ca7312ceb |
parent 1482 | 1a60df4fd63d |
child 1484 | b43cd8a8061f |
--- 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 =