# HG changeset patch
# User wenzelm
# Date 877706354 -7200
# Node ID 86c5bda38e9f5bd0317b6df00fb648006516e8be
# Parent  6ec8d42082f1c3ec0f2e0531000afe24d33b0441
ProtoPure.flexpair_def;

diff -r 6ec8d42082f1 -r 86c5bda38e9f src/Pure/Thy/thm_database.ML
--- 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) =