| changeset 20666 | 82638257d372 |
| parent 20508 | 8182d961c7cc |
| child 21565 | bd28361f4c5b |
--- 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]));