--- 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