src/Pure/conjunction.ML
changeset 24976 821628d16552
parent 24241 424cb8b5e5b4
child 26424 a6cad32a27b0
     1.1 --- a/src/Pure/conjunction.ML	Thu Oct 11 18:58:34 2007 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Thu Oct 11 19:10:17 2007 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  val ABC = read_prop "A ==> B ==> C";
     1.5  val A_B = read_prop "A && B";
     1.6  
     1.7 -val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
     1.8 +val conjunction_def = Thm.unvarify ProtoPure.conjunction_def;
     1.9  
    1.10  fun conjunctionD which =
    1.11    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP