--- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri May 24 17:00:46 2013 +0200
@@ -85,7 +85,7 @@
(* The result of the quantifier elimination *)
val (th, tac) = case prop_of pre_thm of
Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
- let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
+ let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^
Syntax.string_of_term ctxt t1);