author | wenzelm |
Wed, 02 Apr 1997 17:28:27 +0200 | |
changeset 2878 | bf7b6833e4d7 |
parent 2877 | 6476784dba1c |
child 2879 | 477bfcb022d8 |
src/Pure/goals.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/goals.ML Wed Apr 02 15:39:44 1997 +0200 +++ b/src/Pure/goals.ML Wed Apr 02 17:28:27 1997 +0200 @@ -95,7 +95,7 @@ ref((fn _=> error"No goal has been supplied in subgoal module") : bool*thm->thm); -val dummy = trivial(read_cterm Sign.proto_pure +val dummy = trivial(read_cterm Sign.pure ("PROP No_goal_has_been_supplied",propT)); (*List of previous goal stacks, for the undo operation. Set by setstate.