src/HOL/Tools/Function/partial_function.ML

 *)
 
 signature PARTIAL_FUNCTION =
 sig
   val init: string -> term -> term -> thm -> thm -> thm option -> declaration
-
   val mono_tac: Proof.context -> int -> tactic
-
   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 ->
     Attrib.binding * string -> local_theory -> local_theory
 end;
 
-
 structure Partial_Function: PARTIAL_FUNCTION =
 struct
 
 (*** Context Data ***)
 
-datatype setup_data = Setup_Data of 
+datatype setup_data = Setup_Data of
  {fixp: term,
   mono: term,
   fixp_eq: thm,
   fixp_induct: thm,
   fixp_induct_user: thm option};
+
+fun transform_setup_data phi (Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user}) =
+  let
+    val term = Morphism.term phi;
+    val thm = Morphism.thm phi;
+  in
+    Setup_Data
+     {fixp = term fixp, mono = term mono, fixp_eq = thm fixp_eq,
+      fixp_induct = thm fixp_induct, fixp_induct_user = Option.map thm fixp_induct_user}
+  end;
 
 structure Modes = Generic_Data
 (
   type T = setup_data Symtab.table;
   val empty = Symtab.empty;

   fun merge data = Symtab.merge (K true) data;
 )
 
 fun init mode fixp mono fixp_eq fixp_induct fixp_induct_user phi =
   let
-    val term = Morphism.term phi;
-    val thm = Morphism.thm phi;
-    val data' = Setup_Data 
-      {fixp=term fixp, mono=term mono, fixp_eq=thm fixp_eq,
-       fixp_induct=thm fixp_induct, fixp_induct_user=Option.map thm fixp_induct_user};
-  in
-    Modes.map (Symtab.update (mode, data'))
-  end
+    val data' =
+      Setup_Data
+       {fixp = fixp, mono = mono, fixp_eq = fixp_eq,
+        fixp_induct = fixp_induct, fixp_induct_user = fixp_induct_user}
+      |> transform_setup_data (phi $> Morphism.trim_context_morphism);
+  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;
+
+fun lookup_mode ctxt =
+  Symtab.lookup (Modes.get (Context.Proof ctxt))
+  #> Option.map (transform_setup_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
 
 
 (*** Automated monotonicity proofs ***)
 
 fun strip_cases ctac = ctac #> Seq.map snd;

   curry induction predicate *)
 fun specialize_fixp_induct ctxt args fT fT_uc F curry uncurry mono_thm f_def rule =
   let
     val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
     val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
-  in 
+  in
     (* FIXME ctxt vs. ctxt' (!?) *)
     rule
     |> infer_instantiate' ctxt
       ((map o Option.map) (Thm.cterm_of ctxt) [SOME uncurry, NONE, SOME curry, NONE, SOME P_inst])
     |> Tactic.rule_by_tactic ctxt

     val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
 
     val split_paired_all_conv =
       Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all}))
 
-    val split_params_conv = 
+    val split_params_conv =
       Conv.params_conv ~1 (fn ctxt' =>
         Conv.implies_conv split_paired_all_conv Conv.all_conv)
 
     val (P_var, x_var) =
        Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop

       |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
       |> singleton (Variable.export ctxt' ctxt)
   in
     inst_rule'
   end;
-    
+
 
 (*** partial_function definition ***)
 
 fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
   let

     val unfold =
       (infer_instantiate' lthy' (map (SOME o Thm.cterm_of lthy') [uncurry, F, curry]) fixp_eq
         OF [inst_mono_thm, f_def])
       |> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
 
-    val specialized_fixp_induct = 
+    val specialized_fixp_induct =
       specialize_fixp_induct lthy' args fT fT_uc F curry uncurry inst_mono_thm f_def fixp_induct
       |> Drule.rename_bvars' (map SOME (fname :: fname :: argnames));
 
     val mk_raw_induct =
       infer_instantiate' args_ctxt

     lthy'
     |> Local_Theory.note (eq_abinding, [rec_rule])
     |-> (fn (_, rec') =>
       Spec_Rules.add Spec_Rules.Equational ([f], rec')
       #> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec') #> snd)
-    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "mono"), []), [mono_thm]) #> snd) 
+    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "mono"), []), [mono_thm]) #> snd)
     |> (case raw_induct of NONE => I | SOME thm =>
          Local_Theory.note ((Binding.qualify true fname (Binding.name "raw_induct"), []), [thm]) #> snd)
-    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "fixp_induct"), []), [specialized_fixp_induct]) #> snd) 
+    |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "fixp_induct"), []), [specialized_fixp_induct]) #> snd)
   end;
 
 val add_partial_function = gen_add_partial_function Specification.check_spec;
 val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
 

 val _ =
   Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
     ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
       >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
 
-end
+end;