--- a/src/FOLP/IFOLP.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/FOLP/IFOLP.thy Sat May 25 15:37:53 2013 +0200
@@ -66,13 +66,13 @@
parse_translation {*
let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p
- in [(@{syntax_const "_Proof"}, proof_tr)] end
+ in [(@{syntax_const "_Proof"}, K proof_tr)] end
*}
(*show_proofs = true displays the proof terms -- they are ENORMOUS*)
ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *}
-print_translation (advanced) {*
+print_translation {*
let
fun proof_tr' ctxt [P, p] =
if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P