src/Pure/goals.ML
changeset 10487 97d25c125c61
parent 9573 5cadc8146573
child 10745 0f3537fad0f3
equal deleted inserted replaced
10486:7b07dd104a1a 10487:97d25c125c61
   225 		   cat_lines 
   225 		   cat_lines 
   226 		    (map (Sign.string_of_term sign) 
   226 		    (map (Sign.string_of_term sign) 
   227 		     (filter (fn x => (not (Locale.in_locale [x] sign))) 
   227 		     (filter (fn x => (not (Locale.in_locale [x] sign))) 
   228 		      hyps)))
   228 		      hyps)))
   229 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
   229 	    else if Pattern.matches (#tsig(Sign.rep_sg sign)) 
   230 			            (term_of chorn, prop)
   230 			            (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
   231 		 then final_th
   231 		 then final_th
   232 	    else  !result_error_fn state "proved a different theorem"
   232 	    else  !result_error_fn state "proved a different theorem"
   233         end
   233         end
   234   in
   234   in
   235      if Sign.eq_sg(sign, #sign(rep_thm st0))
   235      if Sign.eq_sg(sign, #sign(rep_thm st0))