--- a/src/HOL/Tools/Function/function.ML Tue Apr 04 23:21:16 2017 +0200
+++ b/src/HOL/Tools/Function/function.ML Wed Apr 05 10:26:28 2017 +0200
@@ -120,7 +120,7 @@
val info =
{ add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
- pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
+ pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', totality=NONE,
fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
pelims=pelims',elims=NONE}
@@ -202,7 +202,8 @@
|-> (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,
- simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases, pelims=pelims, elims=SOME elims}
+ simps=SOME simps, inducts=SOME inducts, termination=termination, totality=SOME totality,
+ cases=cases, pelims=pelims, elims=SOME elims}
in
(info',
lthy
--- a/src/HOL/Tools/Function/function_common.ML Tue Apr 04 23:21:16 2017 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Wed Apr 05 10:26:28 2017 +0200
@@ -22,6 +22,7 @@
simps : thm list option,
inducts : thm list option,
termination : thm,
+ totality : thm option,
cases : thm list,
pelims: thm list list,
elims: thm list list option}
@@ -46,6 +47,7 @@
simps : thm list option,
inducts : thm list option,
termination : thm,
+ totality : thm option,
cases : thm list,
pelims : thm list list,
elims : thm list list option}
@@ -291,7 +293,7 @@
domintros : thm list option}
fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
- simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) =
+ simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
let
val term = Morphism.term phi
val thm = Morphism.thm phi
@@ -301,7 +303,8 @@
fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
pinducts = fact pinducts, simps = Option.map fact simps,
inducts = Option.map fact inducts, termination = thm termination,
- defname = Morphism.binding phi defname, is_partial=is_partial, cases = fact cases,
+ totality = Option.map thm totality, defname = Morphism.binding phi defname,
+ is_partial = is_partial, cases = fact cases,
elims = Option.map (map fact) elims, pelims = map fact pelims }
end