--- a/src/HOL/Tools/function_package/fundef_core.ML Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML Thu Apr 03 16:34:52 2008 +0200
@@ -684,7 +684,7 @@
|> forall_intr (cterm_of thy a)
|> forall_intr (cterm_of thy P)
in
- (subset_induct_all, simple_induct_rule)
+ simple_induct_rule
end
@@ -927,7 +927,7 @@
val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
- val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule"
+ val simple_pinduct = PROFILE "Proving partial induction rule"
(mk_partial_induct_rule newthy globals R complete_thm) xclauses
@@ -940,7 +940,7 @@
in
FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
- psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct],
+ psimps=psimps, simple_pinducts=[simple_pinduct],
termination=total_intro, trsimps=trsimps,
domintros=dom_intros}
end