renamed structure TaskQueue to Task_Queue;
authorwenzelm
Tue, 16 Dec 2008 16:25:20 +0100
changeset 29123 63c25d3964f7
parent 29122 b3bae49a013a
child 29124 ce6f21913e54
renamed structure TaskQueue to Task_Queue;
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);