# HG changeset patch
# User wenzelm
# Date 1229441120 -3600
# Node ID 63c25d3964f78264552a02ff5df335032f1613ce
# Parent  b3bae49a013a9e3133f4d59369cebb57e41b452a
renamed structure TaskQueue to Task_Queue;

diff -r b3bae49a013a -r 63c25d3964f7 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Dec 16 16:25:19 2008 +0100
+++ b/src/Pure/pure_setup.ML	Tue Dec 16 16:25:20 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/pure_setup.ML
-    ID:         $Id$
     Author:     Makarius
 
 Pure theory and ML toplevel setup.
@@ -28,8 +27,8 @@
 
 (* ML toplevel pretty printing *)
 
-install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task));
-install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group));
+install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task));
+install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group));
 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
   map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);