src/HOL/Decision_Procs/ferrack_tac.ML
changeset 52131 366fa32ee2a3
parent 51717 9e7d1c139569
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri May 24 16:42:57 2013 +0200
     1.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri May 24 17:00:46 2013 +0200
     1.3 @@ -85,7 +85,7 @@
     1.4      (* The result of the quantifier elimination *)
     1.5      val (th, tac) = case prop_of pre_thm of
     1.6          Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     1.7 -    let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
     1.8 +    let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
     1.9      in 
    1.10            (trace_msg ("calling procedure with term:\n" ^
    1.11               Syntax.string_of_term ctxt t1);