# HG changeset patch
# User wenzelm
# Date 963773792 -7200
# Node ID df7a4824111eec878adf79de38626e0c2fb14d4d
# Parent  a83f3abbfc93e697be52e4c01d4858027c73248f
tuned;

diff -r a83f3abbfc93 -r df7a4824111e src/HOL/Integ/IntDiv.ML
--- a/src/HOL/Integ/IntDiv.ML	Sun Jul 16 20:56:14 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML	Sun Jul 16 20:56:32 2000 +0200
@@ -92,7 +92,7 @@
 
 (*Proving posDivAlg's termination condition*)
 val [tc] = posDivAlg.tcs;
-goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
+goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc));
 by Auto_tac;
 val lemma = result();