src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 40314 b5ec88d9ac03
parent 38864 4abe644fcea5
child 43333 2bdec7f430d3
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Nov 03 10:20:37 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Nov 03 10:48:55 2010 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4                        else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
     1.5                        else if member (op =) [Gt, Ge] c then Thm.dest_arg1
     1.6                        else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
     1.7 -                      else sys_error "decomp_mpinf: Impossible case!!") fm
     1.8 +                      else raise Fail "decomp_mpinf: Impossible case!!") fm
     1.9               val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
    1.10                 if c = Nox then map (instantiate' [] [SOME fm])
    1.11                                      [minf_P, pinf_P, nmi_P, npi_P, ld_P]