src/HOL/Decision_Procs/ferrack_tac.ML
changeset 56245 84fc7dfa3cd4
parent 55498 cf829d10d1d4
child 58956 a816aa3ff391
     1.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     1.5      (* The result of the quantifier elimination *)
     1.6      val (th, tac) = 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 val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
    1.10      in 
    1.11         ((pth RS iffD2) RS pre_thm,