--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri May 24 16:42:57 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri May 24 17:00:46 2013 +0200
@@ -196,7 +196,7 @@
| NONE =>
let
val (f, args) = strip_comb t
- val args = map (Pattern.eta_long []) args
+ val args = map (Envir.eta_long []) args
val _ = @{assert} (fastype_of t = body_type (fastype_of t))
val f' = lookup_pred f
val Ts = case f' of
@@ -232,7 +232,7 @@
in (resvar, (resname :: names', prem :: prems')) end))
end
in
- map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
+ map (apfst Envir.eta_contract) (flatten' (Envir.eta_long [] t) (names, prems))
end;
(* FIXME: create new predicate name -- does not avoid nameclashing *)