src/Pure/goals.ML
changeset 253 d7130a753ecf
parent 230 ec8a2b6aa8a7
child 545 fc4ff96bb0e9
equal deleted inserted replaced
252:7532f95d7f44 253:d7130a753ecf
   140       fun mkresult (check,state) =
   140       fun mkresult (check,state) =
   141         let val ngoals = nprems_of state
   141         let val ngoals = nprems_of state
   142             val th = implies_intr_list cAs state
   142             val th = implies_intr_list cAs state
   143             val {hyps,prop,sign=sign',...} = rep_thm th
   143             val {hyps,prop,sign=sign',...} = rep_thm th
   144         in  if not check then standard th
   144         in  if not check then standard th
   145 	    else if not (eq_sg(sign,sign')) then result_error state
   145 	    else if not (Sign.eq_sg(sign,sign')) then result_error state
   146 		("Signature of proof state has changed!" ^
   146 		("Signature of proof state has changed!" ^
   147 		 sign_error (sign,sign'))
   147 		 sign_error (sign,sign'))
   148             else if ngoals>0 then result_error state
   148             else if ngoals>0 then result_error state
   149 		(string_of_int ngoals ^ " unsolved goals!")
   149 		(string_of_int ngoals ^ " unsolved goals!")
   150             else if not (null hyps) then result_error state
   150             else if not (null hyps) then result_error state
   154 			                (term_of chorn, prop)
   154 			                (term_of chorn, prop)
   155 		 then  standard th 
   155 		 then  standard th 
   156 	    else  result_error state "proved a different theorem"
   156 	    else  result_error state "proved a different theorem"
   157         end
   157         end
   158   in  
   158   in  
   159      if eq_sg(sign, #sign(rep_thm st0)) 
   159      if Sign.eq_sg(sign, #sign(rep_thm st0)) 
   160      then (prems, st0, mkresult)
   160      then (prems, st0, mkresult)
   161      else error ("Definitions would change the proof state's signature" ^
   161      else error ("Definitions would change the proof state's signature" ^
   162 		 sign_error (sign, #sign(rep_thm st0)))
   162 		 sign_error (sign, #sign(rep_thm st0)))
   163   end
   163   end
   164   handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
   164   handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);