# HG changeset patch
# User haftmann
# Date 1548454427 0
# Node ID 170daa8170bee03662359b3fed565041ce03d1a5
# Parent  ac9704fd0935eb61eed408602257dd79fb7689ed
more correct parenthesing

diff -r ac9704fd0935 -r 170daa8170be src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Jan 25 14:19:19 2019 -0500
+++ b/src/Tools/Code/code_runtime.ML	Fri Jan 25 22:13:47 2019 +0000
@@ -591,13 +591,12 @@
 
 fun print_computation_check ctxt =
   print (fn { of_term_for_typ, ... } => fn prfx =>
-    space_implode " " [
+    enclose "(" ")" (space_implode " " [
       mount_computation_checkN,
       "(Context.proof_of (Context.the_generic_context ()))",
       Long_Name.implode [prfx, generated_computationN, covered_constsN],
       Long_Name.append prfx (of_term_for_typ \<^typ>\<open>prop\<close>)
-    ]) ctxt;
-
+    ])) ctxt;
 
 fun add_all_constrs ctxt (dT as Type (tyco, Ts)) =
   case Code.get_type (Proof_Context.theory_of ctxt) tyco of