removed needless "infer_types" call
authorblanchet
Tue, 11 Sep 2012 16:08:27 +0200
changeset 49279 2fcfc11374ed
parent 49278 718e4ad1517e
child 49280 52413dc96326
removed needless "infer_types" call
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, [])]])