# HG changeset patch
# User wenzelm
# Date 1180631479 -7200
# Node ID 94e9413bd7fc0efe269f78fd96d8a12d3859b4f3
# Parent  37091da05d8e85f0f0ac6d627d2d86c666543948
made aconvc pervasive;

diff -r 37091da05d8e -r 94e9413bd7fc src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu May 31 18:31:36 2007 +0200
+++ b/src/Pure/more_thm.ML	Thu May 31 19:11:19 2007 +0200
@@ -192,4 +192,6 @@
 
 end;
 
+val op aconvc = Thm.aconvc;
+
 structure Thmtab = TableFun(type key = thm val ord = Thm.thm_ord);