# HG changeset patch
# User wenzelm
# Date 1206814447 -3600
# Node ID b90d1fc201de346e525230ce97db1de5dea36e31
# Parent  28dd7c7a9a2efa945dbe8542e4b6cc2760a8c6e9
certify wrt. dynamic context;

diff -r 28dd7c7a9a2e -r b90d1fc201de src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Sat Mar 29 19:14:06 2008 +0100
+++ b/src/Pure/conjunction.ML	Sat Mar 29 19:14:07 2008 +0100
@@ -29,11 +29,11 @@
 
 (** abstract syntax **)
 
-val cert = Thm.cterm_of (Context.the_theory (Context.the_thread_data ()));
-val read_prop = cert o SimpleSyntax.read_prop;
+fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
+val read_prop = certify o SimpleSyntax.read_prop;
 
-val true_prop = cert Logic.true_prop;
-val conjunction = cert Logic.conjunction;
+val true_prop = certify Logic.true_prop;
+val conjunction = certify Logic.conjunction;
 
 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;