src/Pure/goals.ML

 (*Current result maker -- set by "goal", used by "result".  *)
 val curr_mkresult = 
     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. 
   A list of lists!*)
 val undo_list = ref([[(dummy, Sequence.null)]] : gstack list);