# HG changeset patch
# User krauss
# Date 1371339540 -7200
# Node ID 71df93ff010d1a30dd91290f5125043f38006b2c
# Parent  63eec9cea2c7660d0f8746626543a98c354c9c47
export cases rule in the info record

diff -r 63eec9cea2c7 -r 71df93ff010d src/HOL/Tools/Function/function.ML
--- 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 
diff -r 63eec9cea2c7 -r 71df93ff010d src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Jun 15 17:19:23 2013 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Jun 16 01:39:00 2013 +0200
@@ -20,7 +20,8 @@
   pinducts: thm list,
   simps : thm list option,
   inducts : thm list option,
-  termination: thm}
+  termination : thm,
+  cases : thm}
 
 end
 
@@ -40,7 +41,8 @@
   pinducts: thm list,
   simps : thm list option,
   inducts : thm list option,
-  termination: thm}
+  termination : thm,
+  cases : thm}
 
 end
 
@@ -145,7 +147,7 @@
   domintros : thm list option}
 
 fun transform_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
-  simps, inducts, termination, defname, is_partial} : info) phi =
+  simps, inducts, termination, defname, is_partial, cases} : info) phi =
     let
       val term = Morphism.term phi
       val thm = Morphism.thm phi
@@ -156,7 +158,7 @@
         fs = map term fs, R = term R, psimps = fact psimps,
         pinducts = fact pinducts, simps = Option.map fact simps,
         inducts = Option.map fact inducts, termination = thm termination,
-        defname = name defname, is_partial=is_partial }
+        defname = name defname, is_partial=is_partial, cases = thm cases }
     end
 
 (* FIXME just one data slot (record) per program unit *)