src/Pure/conjunction.ML
changeset 20238 7e17d70a9303
parent 19416 4198e7698f6a
child 20249 a13adb4f94dc
     1.1 --- a/src/Pure/conjunction.ML	Thu Jul 27 14:21:57 2006 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Thu Jul 27 15:33:21 2006 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  val ABC = read "PROP A ==> PROP B ==> PROP C";
     1.5  val A_B = read "PROP ProtoPure.conjunction(A, B)"
     1.6  
     1.7 -val conjunction_def = #1 (freeze_thaw ProtoPure.conjunction_def);
     1.8 +val conjunction_def = Drule.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