# HG changeset patch
# User wenzelm
# Date 1464789722 -7200
# Node ID 82cd1d481eb95100d66744018aebfde5063aae03
# Parent  3251e9dfea91ba873c76bf63c9bd75c9a359791b
ML pp for Rat.rat;

diff -r 3251e9dfea91 -r 82cd1d481eb9 src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Wed Jun 01 15:33:45 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 16:02:02 2016 +0200
@@ -108,3 +108,5 @@
 ML_system_overload (fn (a, b) => Rat.lt b a) ">";
 ML_system_overload (fn (a, b) => Rat.le b a) ">=";
 ML_system_overload (not o Rat.eq) "<>";
+
+ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));
diff -r 3251e9dfea91 -r 82cd1d481eb9 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jun 01 15:33:45 2016 +0200
+++ b/src/Pure/ROOT.ML	Wed Jun 01 16:02:02 2016 +0200
@@ -52,7 +52,6 @@
 subsection "Library of general tools";
 
 ML_file "General/integer.ML";
-ML_file "General/rat.ML";
 ML_file "General/stack.ML";
 ML_file "General/queue.ML";
 ML_file "General/heap.ML";
@@ -62,6 +61,7 @@
 ML_file "General/linear_set.ML";
 ML_file "General/buffer.ML";
 ML_file "General/pretty.ML";
+ML_file "General/rat.ML";
 ML_file "PIDE/xml.ML";
 ML_file "General/path.ML";
 ML_file "General/url.ML";