--- 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