src/HOL/Tools/Function/partial_function.ML

 *)
 
 signature PARTIAL_FUNCTION =
 sig
   val setup: theory -> theory
-  val init: term -> term -> thm -> declaration
+  val init: string -> term -> term -> thm -> declaration
 
   val add_partial_function: string -> (binding * typ option * mixfix) list ->
     Attrib.binding * term -> local_theory -> local_theory
 
   val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->

   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
 )
 
-fun init fixp mono fixp_eq phi =
+fun init mode fixp mono fixp_eq phi =
   let
     val term = Morphism.term phi;
     val data' = ((term fixp, term mono), Morphism.thm phi fixp_eq);
-    val mode = (* extract mode identifier from morphism prefix! *)
-      Binding.prefix_of (Morphism.binding phi (Binding.empty))
-      |> map fst |> space_implode ".";
-  in
-    if mode = "" then I
-    else Modes.map (Symtab.update (mode, data'))
+  in
+    Modes.map (Symtab.update (mode, data'))
   end
 
 val known_modes = Symtab.keys o Modes.get o Context.Proof;
 val lookup_mode = Symtab.lookup o Modes.get o Context.Proof;