src/Pure/conjunction.ML
changeset 26485 b90d1fc201de
parent 26424 a6cad32a27b0
child 26653 60e0cf6bef89
     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