# HG changeset patch
# User krauss
# Date 1379016617 -7200
# Node ID 8c51fc24d83cfb930143d410007501a4d1c74615
# Parent  cdc780645a49203b71877838dc042c4bef62fe0d
omit automatic Induct.cases_pred declaration, which breaks many existing proofs

diff -r cdc780645a49 -r 8c51fc24d83c src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Sep 10 20:34:32 2013 +0200
+++ b/src/HOL/Tools/Function/function.ML	Thu Sep 12 22:10:17 2013 +0200
@@ -211,7 +211,7 @@
            ((qualify "induct",
              [Attrib.internal (K (Rule_Cases.case_names case_names))]),
             tinduct)
-        ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1, Induct.cases_pred defname]) (fnames ~~ telims)
+        ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ telims)
         |-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
           let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
             case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,