--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Fri Mar 21 20:33:56 2014 +0100
@@ -86,8 +86,8 @@
| retype_free _ t = raise TERM ("retype_free", [t]);
fun drop_all t =
- subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
- strip_qnt_body @{const_name all} t);
+ subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev,
+ strip_qnt_body @{const_name Pure.all} t);
fun permute_args n t =
list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n);