src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -33,12 +33,12 @@
     1.4               {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
     1.5  let
     1.6   fun uset (vars as (x::vs)) p = case term_of p of
     1.7 -   Const(@{const_name "op &"}, _)$ _ $ _ =>
     1.8 +   Const(@{const_name HOL.conj}, _)$ _ $ _ =>
     1.9       let
    1.10         val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    1.11         val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    1.12       in (lS@rS, Drule.binop_cong_rule b lth rth) end
    1.13 - |  Const(@{const_name "op |"}, _)$ _ $ _ =>
    1.14 + |  Const(@{const_name HOL.disj}, _)$ _ $ _ =>
    1.15       let
    1.16         val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    1.17         val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    1.18 @@ -122,12 +122,12 @@
    1.19  
    1.20     fun decomp_mpinf fm =
    1.21       case term_of fm of
    1.22 -       Const(@{const_name "op &"},_)$_$_ =>
    1.23 +       Const(@{const_name HOL.conj},_)$_$_ =>
    1.24          let val (p,q) = Thm.dest_binop fm
    1.25          in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
    1.26                           (Thm.cabs x p) (Thm.cabs x q))
    1.27          end
    1.28 -     | Const(@{const_name "op |"},_)$_$_ =>
    1.29 +     | Const(@{const_name HOL.disj},_)$_$_ =>
    1.30          let val (p,q) = Thm.dest_binop fm
    1.31          in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
    1.32                           (Thm.cabs x p) (Thm.cabs x q))
    1.33 @@ -181,8 +181,8 @@
    1.34     | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    1.35     | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.36     | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.37 -   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    1.38 -   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    1.39 +   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
    1.40 +   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
    1.41     | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    1.42     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    1.43     | Const ("==", _) $ _ $ _ => find_args bounds tm