author | wenzelm |
Fri, 24 Oct 1997 17:14:02 +0200 | |
changeset 3992 | 8b87ba92f7a1 |
parent 3991 | 4cb2f2422695 |
child 3993 | f88e0f0e2666 |
src/Pure/goals.ML | file | annotate | diff | comparison | revisions |
--- 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.