more correct parenthesing
authorhaftmann
Fri Jan 25 22:13:47 2019 +0000 (5 months ago)
changeset 69742170daa8170be
parent 69741 ac9704fd0935
child 69743 6a9a8ef5e4c6
more correct parenthesing
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Jan 25 14:19:19 2019 -0500
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Jan 25 22:13:47 2019 +0000
     1.3 @@ -591,13 +591,12 @@
     1.4  
     1.5  fun print_computation_check ctxt =
     1.6    print (fn { of_term_for_typ, ... } => fn prfx =>
     1.7 -    space_implode " " [
     1.8 +    enclose "(" ")" (space_implode " " [
     1.9        mount_computation_checkN,
    1.10        "(Context.proof_of (Context.the_generic_context ()))",
    1.11        Long_Name.implode [prfx, generated_computationN, covered_constsN],
    1.12        Long_Name.append prfx (of_term_for_typ \<^typ>\<open>prop\<close>)
    1.13 -    ]) ctxt;
    1.14 -
    1.15 +    ])) ctxt;
    1.16  
    1.17  fun add_all_constrs ctxt (dT as Type (tyco, Ts)) =
    1.18    case Code.get_type (Proof_Context.theory_of ctxt) tyco of