certify wrt. dynamic context;
authorwenzelm
Sat Mar 29 19:14:07 2008 +0100 (2008-03-29)
changeset 26485b90d1fc201de
parent 26484 28dd7c7a9a2e
child 26486 b65a5272b360
certify wrt. dynamic context;
src/Pure/conjunction.ML
     1.1 --- a/src/Pure/conjunction.ML	Sat Mar 29 19:14:06 2008 +0100
     1.2 +++ b/src/Pure/conjunction.ML	Sat Mar 29 19:14:07 2008 +0100
     1.3 @@ -29,11 +29,11 @@
     1.4  
     1.5  (** abstract syntax **)
     1.6  
     1.7 -val cert = Thm.cterm_of (Context.the_theory (Context.the_thread_data ()));
     1.8 -val read_prop = cert o SimpleSyntax.read_prop;
     1.9 +fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
    1.10 +val read_prop = certify o SimpleSyntax.read_prop;
    1.11  
    1.12 -val true_prop = cert Logic.true_prop;
    1.13 -val conjunction = cert Logic.conjunction;
    1.14 +val true_prop = certify Logic.true_prop;
    1.15 +val conjunction = certify Logic.conjunction;
    1.16  
    1.17  fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    1.18