# HG changeset patch # User wenzelm # Date 1126642770 -7200 # Node ID 2923018471c26ce69b858f412e16313e7409699f # Parent 9ea1e21797867ec634f277522d029af9b4383116 added stack.ML; diff -r 9ea1e2179786 -r 2923018471c2 src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Tue Sep 13 22:19:29 2005 +0200 +++ b/src/Pure/General/ROOT.ML Tue Sep 13 22:19:30 2005 +0200 @@ -4,6 +4,7 @@ Library of general tools --- prefer this over the 'Standard ML Library'. *) +use "stack.ML"; use "ord_list.ML"; use "alist.ML"; use "table.ML";