# HG changeset patch
# User haftmann
# Date 1515017926 -3600
# Node ID b164fdbb423db6c911f6e84867026d8a24946991
# Parent  4254cfd15b00ff9e9cd9141e5348795d6a5fea57
more correct parentheses

diff -r 4254cfd15b00 -r b164fdbb423d src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Jan 03 22:29:31 2018 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Jan 03 23:18:46 2018 +0100
@@ -579,13 +579,13 @@
 
 fun print_computation kind ctxt T =
   print (fn { of_term_for_typ, ... } => fn prfx =>
-    space_implode " " [
+    enclose "(" ")" (space_implode " " [
       kind,
       "(Context.proof_of (Context.the_generic_context ()))",
       Long_Name.implode [prfx, generated_computationN, covered_constsN],
       (ML_Syntax.atomic o ML_Syntax.print_typ) T,
       Long_Name.append prfx (of_term_for_typ T)
-    ]) ctxt;
+    ])) ctxt;
 
 fun print_computation_check ctxt =
   print (fn { of_term_for_typ, ... } => fn prfx =>