--- a/src/HOL/Tools/Function/function.ML Sat Jun 15 17:19:23 2013 +0200
+++ b/src/HOL/Tools/Function/function.ML Sun Jun 16 01:39:00 2013 +0200
@@ -105,7 +105,7 @@
val addsmps = add_simps fnames post sort_cont
- val (((psimps', [pinducts']), (_, [termination'])), lthy) =
+ val ((((psimps', [pinducts']), [termination']), [cases']), lthy) =
lthy
|> addsmps (conceal_partial o Binding.qualify false "partial")
"psimps" conceal_partial psimp_attribs psimps
@@ -114,15 +114,15 @@
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
Attrib.internal (K (Induct.induct_pred ""))])))]
- ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
- ||> (snd o Local_Theory.note ((qualify "cases",
+ ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]))
+ ||>> (apfst snd o Local_Theory.note ((qualify "cases",
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
||> (case domintros of NONE => I | SOME thms =>
Local_Theory.note ((qualify "domintros", []), thms) #> snd)
val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
- fs=fs, R=R, defname=defname, is_partial=true }
+ fs=fs, R=R, defname=defname, is_partial=true, cases=cases'}
val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
in
@@ -180,7 +180,7 @@
| NONE => error "Not a function"))
val { termination, fs, R, add_simps, case_names, psimps,
- pinducts, defname, ...} = info
+ pinducts, defname, cases, ...} = info
val domT = domain_type (fastype_of R)
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
fun afterqed [[totality]] lthy =
@@ -204,7 +204,7 @@
|-> (fn (simps, (_, inducts)) => fn lthy =>
let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
- simps=SOME simps, inducts=SOME inducts, termination=termination }
+ simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases }
in
(info',
lthy