src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42680 b6c27cf04fe9
parent 42647 59142dbfa3ba
child 42751 f42fd9754724
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed May 04 18:48:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed May 04 19:35:48 2011 +0200
     1.3 @@ -176,8 +176,8 @@
     1.4  
     1.5  fun is_unsound_proof type_sys conjecture_shape facts_offset fact_names =
     1.6    not o is_conjecture_referred_to_in_proof conjecture_shape andf
     1.7 -  forall (is_global_locality o snd)
     1.8 -  o used_facts_in_atp_proof type_sys facts_offset fact_names
     1.9 +  forall (is_locality_global o snd)
    1.10 +    o used_facts_in_atp_proof type_sys facts_offset fact_names
    1.11  
    1.12  (** Soft-core proof reconstruction: Metis one-liner **)
    1.13