src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 43333 2bdec7f430d3
parent 40314 b5ec88d9ac03
child 45654 cf10bde35973
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jun 09 22:25:25 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Jun 09 23:12:02 2011 +0200
     1.3 @@ -67,8 +67,8 @@
     1.4     fun fw mi th th' th'' =
     1.5       let
     1.6        val th0 = if mi then
     1.7 -           instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
     1.8 -        else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
     1.9 +           Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
    1.10 +        else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
    1.11       in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
    1.12    in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
    1.13        fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
    1.14 @@ -114,11 +114,11 @@
    1.15     val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
    1.16          pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
    1.17     val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
    1.18 -        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (instantiate ([],[(U_v,cU)])) nmi
    1.19 +        nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi
    1.20     val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
    1.21 -        npi_le, npi_gt, npi_ge, npi_P] = map (instantiate ([],[(U_v,cU)])) npi
    1.22 +        npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi
    1.23     val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
    1.24 -        ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
    1.25 +        ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld
    1.26  
    1.27     fun decomp_mpinf fm =
    1.28       case term_of fm of