src/FOLP/IFOLP.thy
changeset 42616 92715b528e78
parent 41310 65631ca437c9
child 42799 4e33894aec6d
     1.1 --- a/src/FOLP/IFOLP.thy	Mon May 02 13:29:47 2011 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Mon May 02 16:33:21 2011 +0200
     1.3 @@ -69,8 +69,7 @@
     1.4  *}
     1.5  
     1.6  (*show_proofs = true displays the proof terms -- they are ENORMOUS*)
     1.7 -ML {* val (show_proofs, setup_show_proofs) = Attrib.config_bool "show_proofs" (K false) *}
     1.8 -setup setup_show_proofs
     1.9 +ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *}
    1.10  
    1.11  print_translation (advanced) {*
    1.12    let