# HG changeset patch
# User wenzelm
# Date 859994907 -7200
# Node ID bf7b6833e4d7fdaf7426840f4d6de87ef7c1eae9
# Parent  6476784dba1c62c6587a62294c5259c3d3a2e59d
changed signature of dummy goal from proto_pure to pure;

diff -r 6476784dba1c -r bf7b6833e4d7 src/Pure/goals.ML
--- 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.