| changeset 3999 | 86c5bda38e9f |
| parent 3976 | 1030dd79720b |
| child 4023 | a9dc0484c903 |
--- a/src/Pure/Thy/thm_database.ML Fri Oct 24 17:18:49 1997 +0200 +++ b/src/Pure/Thy/thm_database.ML Fri Oct 24 17:19:14 1997 +0200 @@ -302,7 +302,7 @@ (*Store result of proof in loaded_thys and as ML value*) -val qed_thm = ref flexpair_def(*dummy*); +val qed_thm = ref ProtoPure.flexpair_def(*dummy*); fun bind_thm (name, thm) =