src/Pure/goals.ML

 	    		handle THM _ => state   (*smash flexflex pairs*)
 	    val ngoals = nprems_of state
             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'))
             else if ngoals>0 then !result_error_ref state
 		(string_of_int ngoals ^ " unsolved goals!")