# HG changeset patch
# User krauss
# Date 1371416204 -7200
# Node ID 80c00a851de590d6314b47d803127bfa385d23ae
# Parent  71df93ff010d1a30dd91290f5125043f38006b2c
export dom predicate in the info record

diff -r 71df93ff010d -r 80c00a851de5 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun Jun 16 01:39:00 2013 +0200
+++ b/src/HOL/Tools/Function/function.ML	Sun Jun 16 22:56:44 2013 +0200
@@ -94,7 +94,7 @@
 
     fun afterqed [[proof]] lthy =
       let
-        val FunctionResult {fs, R, psimps, simple_pinducts,
+        val FunctionResult {fs, R, dom, psimps, simple_pinducts,
           termination, domintros, cases, ...} =
           cont (Thm.close_derivation proof)
 
@@ -122,7 +122,7 @@
 
         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, cases=cases'}
+          fs=fs, R=R, dom=dom, 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, cases, ...} = info
+      pinducts, defname, cases, dom, ...} = 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 =
@@ -203,7 +203,7 @@
             tinduct)
         |-> (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,
+            case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
             simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases }
           in
             (info',
diff -r 71df93ff010d -r 80c00a851de5 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sun Jun 16 01:39:00 2013 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Jun 16 22:56:44 2013 +0200
@@ -16,6 +16,7 @@
   case_names : string list,
   fs : term list,
   R : term,
+  dom: term,
   psimps: thm list,
   pinducts: thm list,
   simps : thm list option,
@@ -37,6 +38,7 @@
   case_names : string list,
   fs : term list,
   R : term,
+  dom: term,
   psimps: thm list,
   pinducts: thm list,
   simps : thm list option,
@@ -61,6 +63,7 @@
    {fs: term list,
     G: term,
     R: term,
+    dom: term,
     psimps : thm list,
     simple_pinducts : thm list,
     cases : thm,
@@ -140,13 +143,14 @@
  {fs: term list,
   G: term,
   R: term,
+  dom: term,
   psimps : thm list,
   simple_pinducts : thm list,
   cases : thm,
   termination : thm,
   domintros : thm list option}
 
-fun transform_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
+fun transform_function_data ({add_simps, case_names, fs, R, dom, psimps, pinducts,
   simps, inducts, termination, defname, is_partial, cases} : info) phi =
     let
       val term = Morphism.term phi
@@ -155,7 +159,7 @@
       val name = Binding.name_of o Morphism.binding phi o Binding.name
     in
       { add_simps = add_simps, case_names = case_names,
-        fs = map term fs, R = term R, psimps = fact psimps,
+        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 = name defname, is_partial=is_partial, cases = thm cases }
diff -r 71df93ff010d -r 80c00a851de5 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Jun 16 01:39:00 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Jun 16 22:56:44 2013 +0200
@@ -863,8 +863,9 @@
     val ((R, RIntro_thmss, R_elim), lthy) =
       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
 
+    val dom = mk_acc domT R
     val (_, lthy) =
-      Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
+      Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), dom) lthy
 
     val newthy = Proof_Context.theory_of lthy
     val clauses = map (transfer_clause_ctx newthy) clauses
@@ -914,7 +915,7 @@
              (map (mk_domain_intro lthy globals R R_elim)) xclauses)
            else NONE
       in
-        FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
+        FunctionResult {fs=[f], G=G, R=R, dom=dom, cases=complete_thm,
           psimps=psimps, simple_pinducts=[simple_pinduct],
           termination=total_intro, domintros=dom_intros}
       end
diff -r 71df93ff010d -r 80c00a851de5 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun Jun 16 01:39:00 2013 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun Jun 16 22:56:44 2013 +0200
@@ -252,7 +252,7 @@
   let
     val result = inner_cont proof
     val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
-      termination, domintros, ...} = result
+      termination, domintros, dom, ...} = result
 
     val (all_f_defs, fs) =
       map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -272,7 +272,7 @@
     val mtermination = full_simplify rew_simpset termination
     val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros
   in
-    FunctionResult { fs=fs, G=G, R=R,
+    FunctionResult { fs=fs, G=G, R=R, dom=dom,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
       domintros=mdomintros}