# HG changeset patch
# User blanchet
# Date 1347372507 -7200
# Node ID 2fcfc11374ed93e30b9746f976d13f8439dc30b2
# Parent  718e4ad1517ede7fe0b2f37b68ded88a7557c385
removed needless "infer_types" call

diff -r 718e4ad1517e -r 2fcfc11374ed src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 11 14:51:52 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 11 16:08:27 2012 +0200
@@ -1182,8 +1182,7 @@
     map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
       goals (map (unfold_defs_tac lthy defs) tacs)
     |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
-  end) oo prepare_def const_policy fact_policy qualify
-  (singleton o Type_Infer_Context.infer_types) Ds;
+  end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
 
 val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
   Proof.unfolding ([[(defs, [])]])