src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 38558 32ad17fe2b9c
parent 38549 d0385f2764d8
child 38786 e46e7a9cb622
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 16:08:54 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 19 16:08:59 2010 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4   fun main vs p =
     1.5    let
     1.6     val ((xn,ce),(x,fm)) = (case term_of p of
     1.7 -                   Const(@{const_name "Ex"},_)$Abs(xn,xT,_) =>
     1.8 +                   Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
     1.9                          Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
    1.10                   | _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
    1.11     val cT = ctyp_of_term x
    1.12 @@ -178,16 +178,16 @@
    1.13       Const (@{const_name "op ="}, T) $ _ $ _ =>
    1.14         if domain_type T = HOLogic.boolT then find_args bounds tm
    1.15         else Thm.dest_fun2 tm
    1.16 -   | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
    1.17 -   | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.18 -   | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.19 +   | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    1.20 +   | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.21 +   | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.22     | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    1.23     | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    1.24     | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    1.25     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    1.26     | Const ("==", _) $ _ $ _ => find_args bounds tm
    1.27     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    1.28 -   | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
    1.29 +   | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
    1.30     | _ => Thm.dest_fun2 tm)
    1.31    and find_args bounds tm =
    1.32             (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)