Pure.thy;
authorwenzelm
Fri, 24 Oct 1997 17:14:02 +0200
changeset 3992 8b87ba92f7a1
parent 3991 4cb2f2422695
child 3993 f88e0f0e2666
Pure.thy;
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.