# HG changeset patch
# User wenzelm
# Date 882521922 -3600
# Node ID 02730662e4464e1885093866bda501d08a1b158d
# Parent  ecfeff48bf0c026ca60765467ae6f6cd41f05ab2
Term.termless;

diff -r ecfeff48bf0c -r 02730662e446 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 19 09:58:03 1997 +0100
+++ b/src/Pure/thm.ML	Fri Dec 19 09:58:42 1997 +0100
@@ -1524,7 +1524,7 @@
     prems = prems, mk_rews = mk_rews, termless = termless};
 
 val empty_mss =
-  mk_mss (Net.empty, [], Net.empty, [], [], K [], Logic.termless);
+  mk_mss (Net.empty, [], Net.empty, [], [], K [], Term.termless);