# HG changeset patch
# User wenzelm
# Date 1419259816 -3600
# Node ID 15a73dd9df51171cdff4397413d055a6783e89a3
# Parent  cdcbda56b05b7073f2c8c98c1d971e0170ac44bf
tuned;

diff -r cdcbda56b05b -r 15a73dd9df51 src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Mon Dec 22 14:35:42 2014 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML	Mon Dec 22 15:50:16 2014 +0100
@@ -142,10 +142,11 @@
     val t' = approx 30 ctxt t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = Print_Mode.with_modes modes (fn () =>
+  in
+    Print_Mode.with_modes modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
-  in Pretty.writeln p end;
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ()
+  end |> Pretty.writeln;
 
 val opt_modes =
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];