Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
certify wrt. dynamic context;
authorwenzelm
Sat, 29 Mar 2008 19:14:07 +0100
changeset 26485 b90d1fc201de
parent 26484 28dd7c7a9a2e
child 26486 b65a5272b360
certify wrt. dynamic context;
src/Pure/conjunction.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle