src/Pure/conjunction.ML
changeset 33384 1b5ba4e6a953
parent 33277 1bdc3c732fdd
child 35845 e5980f0ad025
     1.1 --- a/src/Pure/conjunction.ML	Mon Nov 02 20:30:40 2009 +0100
     1.2 +++ b/src/Pure/conjunction.ML	Mon Nov 02 20:34:59 2009 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  (** abstract syntax **)
     1.5  
     1.6  fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
     1.7 -val read_prop = certify o SimpleSyntax.read_prop;
     1.8 +val read_prop = certify o Simple_Syntax.read_prop;
     1.9  
    1.10  val true_prop = certify Logic.true_prop;
    1.11  val conjunction = certify Logic.conjunction;