# HG changeset patch
# User chaieb
# Date 1193829581 -3600
# Node ID 833abbc3e7335cff0da140be2b6cee4b3dbba03f
# Parent  759bffe1d416b03d4105b488f94259a54cf9188e
tuned

diff -r 759bffe1d416 -r 833abbc3e733 src/HOL/Tools/Groebner_Basis/misc.ML
--- a/src/HOL/Tools/Groebner_Basis/misc.ML	Wed Oct 31 12:19:37 2007 +0100
+++ b/src/HOL/Tools/Groebner_Basis/misc.ML	Wed Oct 31 12:19:41 2007 +0100
@@ -17,7 +17,7 @@
 
 fun is_binop ct ct' =
   (case Thm.term_of ct' of
-    c $ _ $ _ => Thm.term_of ct aconv c
+    c $ _ $ _ => term_of ct aconv c
   | _ => false);
 
 fun dest_binop ct ct' =