Removed "standard" call from uresult, to allow specialist applications
authorpaulson
Fri, 08 Nov 1996 14:07:56 +0100
changeset 2169 31ba286f2307
parent 2168 fcf18ada8904
child 2170 c5e460f1ebb4
Removed "standard" call from uresult, to allow specialist applications
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'))