--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 16:29:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 16:43:46 2013 +0200
@@ -230,7 +230,7 @@
(case Term.strip_comb t of
(Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
| (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
- fld (conds @ conjuncts cond) then_branch
+ fld (conds @ HOLogic.conjuncts cond) then_branch
o fld (conds @ s_not_disj cond) else_branch
| (Const (c, _), args as _ :: _) =>
let val n = num_binder_types (Sign.the_const_type thy c) in
@@ -239,7 +239,7 @@
(case dest_case ctxt s Ts t of
NONE => f conds t
| SOME (conds', branches) =>
- fold_rev (uncurry fld) (map (append conds o conjuncts) conds' ~~ branches))
+ fold_rev (uncurry fld) (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
| _ => f conds t)
end
| _ => f conds t)