equal
deleted
inserted
replaced
98 (*Current result maker -- set by "goal", used by "result". *) |
98 (*Current result maker -- set by "goal", used by "result". *) |
99 val curr_mkresult = |
99 val curr_mkresult = |
100 ref((fn _=> error"No goal has been supplied in subgoal module") |
100 ref((fn _=> error"No goal has been supplied in subgoal module") |
101 : bool*thm->thm); |
101 : bool*thm->thm); |
102 |
102 |
103 val dummy = trivial(read_cterm Sign.pure |
103 val dummy = trivial(read_cterm Sign.proto_pure |
104 ("PROP No_goal_has_been_supplied",propT)); |
104 ("PROP No_goal_has_been_supplied",propT)); |
105 |
105 |
106 (*List of previous goal stacks, for the undo operation. Set by setstate. |
106 (*List of previous goal stacks, for the undo operation. Set by setstate. |
107 A list of lists!*) |
107 A list of lists!*) |
108 val undo_list = ref([[(dummy, Sequence.null)]] : gstack list); |
108 val undo_list = ref([[(dummy, Sequence.null)]] : gstack list); |