clarified string_of_rat operations;

--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 15:19:44 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Wed Jun 01 15:33:45 2016 +0200
@@ -18,15 +18,6 @@
 
 local
 
-fun string_of_rat r =
-  let
-    val (nom, den) = Rat.dest r
-  in
-    if den = 1 then string_of_int nom
-    else string_of_int nom ^ "/" ^ string_of_int den
-  end
-
-
 (* map polynomials to strings *)
 
 fun string_of_varpow x k =
@@ -49,9 +40,9 @@
     in foldr1 (fn (s, t) => s ^ "*" ^ t) vps end
 
 fun string_of_cmonomial (m,c) =
-  if FuncUtil.Ctermfunc.is_empty m then string_of_rat c
+  if FuncUtil.Ctermfunc.is_empty m then Rat.string_of_rat c
   else if c = @1 then string_of_monomial m
-  else string_of_rat c ^ "*" ^ string_of_monomial m
+  else Rat.string_of_rat c ^ "*" ^ string_of_monomial m
 
 fun string_of_poly p =
   if FuncUtil.Monomialfunc.is_empty p then "0"
@@ -67,9 +58,9 @@
 fun pss_to_cert (RealArith.Axiom_eq i) = "A=" ^ string_of_int i
   | pss_to_cert (RealArith.Axiom_le i) = "A<=" ^ string_of_int i
   | pss_to_cert (RealArith.Axiom_lt i) = "A<" ^ string_of_int i
-  | pss_to_cert (RealArith.Rational_eq r) = "R=" ^ string_of_rat r
-  | pss_to_cert (RealArith.Rational_le r) = "R<=" ^ string_of_rat r
-  | pss_to_cert (RealArith.Rational_lt r) = "R<" ^ string_of_rat r
+  | pss_to_cert (RealArith.Rational_eq r) = "R=" ^ Rat.string_of_rat r
+  | pss_to_cert (RealArith.Rational_le r) = "R<=" ^ Rat.string_of_rat r
+  | pss_to_cert (RealArith.Rational_lt r) = "R<" ^ Rat.string_of_rat r
   | pss_to_cert (RealArith.Square p) = "[" ^ string_of_poly p ^ "]^2"
   | pss_to_cert (RealArith.Eqmul (p, pss)) =
       "([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"

--- a/src/Pure/General/rat.ML	Wed Jun 01 15:19:44 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 15:33:45 2016 +0200
@@ -13,6 +13,7 @@
   val make: int * int -> rat
   val dest: rat -> int * int
   val string_of_rat: rat -> string
+  val signed_string_of_rat: rat -> string
   val eq: rat * rat -> bool
   val ord: rat * rat -> order
   val le: rat -> rat -> bool
@@ -48,8 +49,11 @@
 
 fun of_int i = Rat (i, 1);
 
-fun string_of_rat (Rat (p, q)) =
-  string_of_int p ^ "/" ^ string_of_int q;
+fun string_of_rat (Rat (p, 1)) = string_of_int p
+  | string_of_rat (Rat (p, q)) = string_of_int p ^ "/" ^ string_of_int q;
+
+fun signed_string_of_rat (Rat (p, 1)) = signed_string_of_int p
+  | signed_string_of_rat (Rat (p, q)) = signed_string_of_int p ^ "/" ^ string_of_int q;
 
 fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);