# HG changeset patch
# User wenzelm
# Date 1456781524 -3600
# Node ID a62c86d25024fe42dd2f59040d59da5d9153f4f1
# Parent  bc6e771e98a6d3819a84c6ef0644951111a06e41
tuned header;

diff -r bc6e771e98a6 -r a62c86d25024 src/Pure/RAW/ml_heap_polyml-5.3.0.ML
--- a/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Mon Feb 29 21:32:53 2016 +0100
+++ b/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Mon Feb 29 22:32:04 2016 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Pure/RAW/ml_heap.ML
+(*  Title:      Pure/RAW/ml_heap_polyml-5.3.0.ML
     Author:     Makarius
 
 ML heap operations.