# HG changeset patch
# User wenzelm
# Date 877706042 -7200
# Node ID 8b87ba92f7a116f826b9166a81afb8a5c9755128
# Parent  4cb2f2422695dceb8e29e9ee7dd7db44d0c8824d
Pure.thy;

diff -r 4cb2f2422695 -r 8b87ba92f7a1 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Oct 24 17:13:21 1997 +0200
+++ b/src/Pure/goals.ML	Fri Oct 24 17:14:02 1997 +0200
@@ -96,7 +96,7 @@
     ref((fn _=> error"No goal has been supplied in subgoal module") 
        : bool*thm->thm);
 
-val dummy = trivial(read_cterm Sign.pure 
+val dummy = trivial(read_cterm (sign_of Pure.thy)
     ("PROP No_goal_has_been_supplied",propT));
 
 (*List of previous goal stacks, for the undo operation.  Set by setstate.