# 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]));