Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thm.dest_binop;
authorwenzelm
Thu, 21 Sep 2006 19:04:36 +0200
changeset 20666 82638257d372
parent 20665 7e54c7cc72a5
child 20667 953b68f4a9f3
Thm.dest_binop;
src/Pure/conjunction.ML file | annotate | diff | comparison | revisions 
--- 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]));
isabelle