diff -r f66bb6536f6a -r b0d21ae2528e src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Jan 02 23:18:58 2010 +0100
@@ -5,9 +5,49 @@
 Common definitions and other infrastructure.
 *)
 
+signature FUNCTION_DATA =
+sig
+
+type info =
+ {is_partial : bool,
+  defname : string,
+    (* contains no logical entities: invariant under morphisms: *)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  psimps: thm list,
+  pinducts: thm list,
+  termination: thm
+ }  
+
+end
+
+structure Function_Data : FUNCTION_DATA =
+struct
+
+type info =
+ {is_partial : bool,
+  defname : string,
+    (* contains no logical entities: invariant under morphisms: *)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  psimps: thm list,
+  pinducts: thm list,
+  termination: thm
+ }  
+
+end
+
 structure Function_Common =
 struct
 
+open Function_Data
+
 local open Function_Lib in
 
 (* Profiling *)
@@ -58,41 +98,21 @@
       domintros : thm list option
      }
 
-
-datatype function_context_data =
-  FunctionCtxData of
-     {
-      defname : string,
-
-      (* contains no logical entities: invariant under morphisms *)
-      add_simps : (binding -> binding) -> string -> (binding -> binding) ->
-        Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
-
-      case_names : string list,
-
-      fs : term list,
-      R : term,
-      
-      psimps: thm list,
-      pinducts: thm list,
-      termination: thm
-     }
-
-fun morph_function_data (FunctionCtxData {add_simps, case_names, fs, R, 
-                                      psimps, pinducts, termination, defname}) phi =
+fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
+  termination, defname, is_partial} : info) phi =
     let
       val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
       val name = Binding.name_of o Morphism.binding phi o Binding.name
     in
-      FunctionCtxData { add_simps = add_simps, case_names = case_names,
-                      fs = map term fs, R = term R, psimps = fact psimps, 
-                      pinducts = fact pinducts, termination = thm termination,
-                      defname = name defname }
+      { add_simps = add_simps, case_names = case_names,
+        fs = map term fs, R = term R, psimps = fact psimps, 
+        pinducts = fact pinducts, termination = thm termination,
+        defname = name defname, is_partial=is_partial }
     end
 
 structure FunctionData = Generic_Data
 (
-  type T = (term * function_context_data) Item_Net.T;
+  type T = (term * info) Item_Net.T;
   val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   val extend = I;
   fun merge tabs : T = Item_Net.merge tabs;
@@ -135,7 +155,7 @@
 
 val all_function_data = Item_Net.content o get_function
 
-fun add_function_data (data as FunctionCtxData {fs, termination, ...}) =
+fun add_function_data (data : info as {fs, termination, ...}) =
     FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
     #> store_termination_rule termination