# HG changeset patch
# User wenzelm
# Date 1180629096 -7200
# Node ID 37091da05d8e85f0f0ac6d627d2d86c666543948
# Parent  fcdd4346fa6bc3424c7ea99556a827f7243bc3e5
moved aconvc to more_thm.ML;

diff -r fcdd4346fa6b -r 37091da05d8e src/Pure/conv.ML
--- a/src/Pure/conv.ML	Thu May 31 18:16:59 2007 +0200
+++ b/src/Pure/conv.ML	Thu May 31 18:31:36 2007 +0200
@@ -7,11 +7,10 @@
 
 infix 1 then_conv;
 infix 0 else_conv;
-infix aconvc;
+
 signature CONV =
 sig
   type conv = cterm -> thm
-  val aconvc : cterm * cterm -> bool
   val no_conv: conv
   val all_conv: conv
   val then_conv: conv * conv -> conv
@@ -43,8 +42,6 @@
 
 type conv = cterm -> thm;
 
-fun s aconvc t = term_of s aconv term_of t;
-
 fun no_conv _ = raise CTERM ("no conversion", []);
 val all_conv = Thm.reflexive;
 
@@ -106,6 +103,7 @@
 
 fun binop_conv cv = combination_conv (arg_conv cv) cv;
 
+
 (* logic *)
 
 (*rewrite B in !!x1 ... xn. B*)
diff -r fcdd4346fa6b -r 37091da05d8e src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu May 31 18:16:59 2007 +0200
+++ b/src/Pure/more_thm.ML	Thu May 31 18:31:36 2007 +0200
@@ -5,6 +5,8 @@
 Further operations on type ctyp/cterm/thm, outside the inference kernel.
 *)
 
+infix aconvc;
+
 signature THM =
 sig
   include THM
@@ -17,6 +19,7 @@
   val lhs_of: thm -> cterm
   val rhs_of: thm -> cterm
   val thm_ord: thm * thm -> order
+  val aconvc : cterm * cterm -> bool
   val eq_thm: thm * thm -> bool
   val eq_thms: thm list * thm list -> bool
   val eq_thm_thy: thm * thm -> bool
@@ -99,6 +102,8 @@
 
 (* equality *)
 
+val op aconvc = op aconv o pairself Thm.term_of;
+
 fun eq_thm ths =
   Context.joinable (pairself Thm.theory_of_thm ths) andalso
   thm_ord ths = EQUAL;