--- a/src/HOL/Decision_Procs/ferrack_tac.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Thu Aug 19 16:08:59 2010 +0200
@@ -91,7 +91,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case prop_of pre_thm of
- Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^