# HG changeset patch
# User wenzelm
# Date 1158858276 -7200
# Node ID 82638257d37295b3f5932d2dc2995b2d8b3ba55b
# Parent  7e54c7cc72a545165669416f37474b6e2aa8f3a7
Thm.dest_binop;

diff -r 7e54c7cc72a5 -r 82638257d372 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Thu Sep 21 19:04:29 2006 +0200
+++ b/src/Pure/conjunction.ML	Thu Sep 21 19:04:36 2006 +0200
@@ -45,7 +45,7 @@
 
 fun dest_conjunction ct =
   (case Thm.term_of ct of
-    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Drule.dest_binop ct
+    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
   | _ => raise TERM ("dest_conjunction", [term_of ct]));