--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Jun 02 16:23:10 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Jun 02 16:49:44 2016 +0200
@@ -101,8 +101,6 @@
val no_refl: thm list -> thm list
val no_reflexive: thm list -> thm list
- val fold_thms: Proof.context -> thm list -> thm -> thm
-
val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
val parse_map_rel_pred_bindings: (binding * binding * binding) parser
@@ -455,6 +453,4 @@
val no_refl = filter_out is_refl;
val no_reflexive = filter_out Thm.is_reflexive;
-fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
-
end;