# HG changeset patch
# User wenzelm
# Date 1282914455 -7200
# Node ID 34c84817e39c9255cfc743f574d0567d9508f414
# Parent  712cb964d1130b28723e5a7bafb10470d2d44410
proper configuration option "show_proofs";
modernized syntax translation;

diff -r 712cb964d113 -r 34c84817e39c src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Fri Aug 27 14:14:08 2010 +0200
+++ b/src/FOLP/IFOLP.thy	Fri Aug 27 15:07:35 2010 +0200
@@ -63,20 +63,22 @@
 
 syntax "_Proof" :: "[p,o]=>prop"    ("(_ /: _)" [51, 10] 5)
 
-ML {*
-
-(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
-val show_proofs = Unsynchronized.ref false;
-
-fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
-
-fun proof_tr' [P,p] =
-  if ! show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
-  else P  (*this case discards the proof term*);
+parse_translation {*
+  let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p
+  in [(@{syntax_const "_Proof"}, proof_tr)] end
 *}
 
-parse_translation {* [(@{syntax_const "_Proof"}, proof_tr)] *}
-print_translation {* [(@{const_syntax Proof}, proof_tr')] *}
+(*show_proofs = true displays the proof terms -- they are ENORMOUS*)
+ML {* val (show_proofs, setup_show_proofs) = Attrib.config_bool "show_proofs" (K false) *}
+setup setup_show_proofs
+
+print_translation (advanced) {*
+  let
+    fun proof_tr' ctxt [P, p] =
+      if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P
+      else P
+  in [(@{const_syntax Proof}, proof_tr')] end
+*}
 
 axioms