--- a/src/HOL/Decision_Procs/Cooper.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Apr 08 13:31:16 2011 +0200
@@ -1924,12 +1924,12 @@
@{code NOT} (fm_of_term ps vs t')
| fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
let
- val (xn', p') = variant_abs (xn, xT, p);
+ val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *)
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code E} (fm_of_term ps vs' p) end
| fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
let
- val (xn', p') = variant_abs (xn, xT, p);
+ val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *)
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code A} (fm_of_term ps vs' p) end
| fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
@@ -1988,7 +1988,7 @@
else insert (op aconv) t acc
| f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a
else insert (op aconv) t acc
- | Abs p => term_bools acc (snd (variant_abs p))
+ | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p)) (* FIXME !? *)
| _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
end;