# HG changeset patch
# User paulson
# Date 847458476 -3600
# Node ID 31ba286f2307462a6baf08c02626b31dbe8286d6
# Parent  fcf18ada890487e89b92f56cc37c747c6c9fef6c
Removed "standard" call from uresult, to allow specialist applications

diff -r fcf18ada8904 -r 31ba286f2307 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Nov 08 14:04:38 1996 +0100
+++ b/src/Pure/goals.ML	Fri Nov 08 14:07:56 1996 +0100
@@ -142,7 +142,7 @@
             val th = strip_shyps (implies_intr_list cAs state)
             val {hyps,prop,sign=sign',...} = rep_thm th
             val xshyps = extra_shyps th;
-        in  if not check then standard th
+        in  if not check then th
 	    else if not (Sign.eq_sg(sign,sign')) then !result_error_ref state
 		("Signature of proof state has changed!" ^
 		 sign_error (sign,sign'))