# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1491380788 -7200
# Node ID 5dbe02addca5d968ff6758a4bd9b9953b670e570
# Parent  e3fb3036a00ec97d0bd8741665fc5baf651b274a
store totality fact in function info

diff -r e3fb3036a00e -r 5dbe02addca5 src/HOL/Tools/Function/function.ML
--- 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
diff -r e3fb3036a00e -r 5dbe02addca5 src/HOL/Tools/Function/function_common.ML
--- 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