# HG changeset patch # User wenzelm # Date 1220539430 -7200 # Node ID 565be25eb38f4d8cbfe3b709bb9426a59ad53304 # Parent 93ee30a54c9ad03814c2dc1823c04f37a735a87e added General/queue.ML; diff -r 93ee30a54c9a -r 565be25eb38f src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Thu Sep 04 16:43:48 2008 +0200 +++ b/src/Pure/General/ROOT.ML Thu Sep 04 16:43:50 2008 +0200 @@ -22,6 +22,7 @@ use "integer.ML"; use "stack.ML"; +use "queue.ML"; use "heap.ML"; use "ord_list.ML"; use "balanced_tree.ML"; diff -r 93ee30a54c9a -r 565be25eb38f src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Sep 04 16:43:48 2008 +0200 +++ b/src/Pure/IsaMakefile Thu Sep 04 16:43:50 2008 +0200 @@ -29,8 +29,8 @@ General/markup.ML General/name_space.ML General/ord_list.ML \ General/output.ML General/path.ML General/position.ML \ General/pretty.ML General/print_mode.ML General/properties.ML \ - General/scan.ML General/secure.ML General/seq.ML General/source.ML \ - General/stack.ML General/susp.ML General/symbol.ML \ + General/queue.ML General/scan.ML General/secure.ML General/seq.ML \ + General/source.ML General/stack.ML General/susp.ML General/symbol.ML \ General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \ General/yxml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML \ Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \