src/HOL/Decision_Procs/cooper_tac.ML
changeset 56245 84fc7dfa3cd4
parent 55987 52c22561996d
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4      (* The result of the quantifier elimination *)
     1.5      val (th, tac) =
     1.6        (case (prop_of pre_thm) of
     1.7 -        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     1.8 +        Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     1.9            let
    1.10              val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
    1.11            in