src/Pure/conjunction.ML
changeset 20666 82638257d372
parent 20508 8182d961c7cc
child 21565 bd28361f4c5b
     1.1 --- a/src/Pure/conjunction.ML	Thu Sep 21 19:04:29 2006 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Thu Sep 21 19:04:36 2006 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5  fun dest_conjunction ct =
     1.6    (case Thm.term_of ct of
     1.7 -    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Drule.dest_binop ct
     1.8 +    (Const ("ProtoPure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
     1.9    | _ => raise TERM ("dest_conjunction", [term_of ct]));
    1.10  
    1.11