# HG changeset patch
# User blanchet
# Date 1386978330 -28800
# Node ID 7068557b7c6313b59f3e5718f5abb7663a6a4b95
# Parent  6db5fbc0243633254d9196e626243ff01569f567# Parent  010eefa0a4f3485e28d376fa04a814628dab255e
merged

diff -r 6db5fbc02436 -r 7068557b7c63 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -459,7 +459,7 @@
 
 fun bnf_of ctxt =
   Symtab.lookup (Data.get (Context.Proof ctxt))
-  #> Option.map (morph_bnf (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
+  #> Option.map (morph_bnf (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
 
 
 (* Utilities *)
diff -r 6db5fbc02436 -r 7068557b7c63 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -156,7 +156,7 @@
    sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
 
 val transfer_fp_sugar =
-  morph_fp_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 structure Data = Generic_Data
 (
@@ -344,7 +344,7 @@
    (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs));
 
 val transfer_lfp_sugar_thms =
-  morph_lfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 type gfp_sugar_thms =
   ((thm list * thm) list * Args.src list)
@@ -368,7 +368,7 @@
     map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs));
 
 val transfer_gfp_sugar_thms =
-  morph_gfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
 
diff -r 6db5fbc02436 -r 7068557b7c63 src/HOL/BNF/Tools/bnf_fp_n2m.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -370,7 +370,7 @@
         xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
         xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
         rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
-       |> morph_fp_result (Morphism.term_morphism (singleton (Variable.polymorphic lthy))));
+       |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   in
     (fp_res, lthy)
   end;
diff -r 6db5fbc02436 -r 7068557b7c63 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -52,7 +52,7 @@
     Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
 
 val transfer_n2m_sugar =
-  morph_n2m_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_n2m_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 fun n2m_sugar_of ctxt =
   Typtab.lookup (Data.get (Context.Proof ctxt))
@@ -127,7 +127,7 @@
     fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
       let
         val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
-        val phi = Morphism.term_morphism (Term.subst_TVars rho);
+        val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
       in
         morph_ctr_sugar phi (nth ctr_sugars index)
       end;
diff -r 6db5fbc02436 -r 7068557b7c63 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -125,7 +125,7 @@
    case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
 
 val transfer_ctr_sugar =
-  morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_ctr_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 structure Data = Generic_Data
 (
diff -r 6db5fbc02436 -r 7068557b7c63 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -189,8 +189,11 @@
   let
     fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
   in
-    Morphism.thm_morphism f $> Morphism.term_morphism term
-    $> Morphism.typ_morphism (Logic.type_map term)
+    Morphism.morphism "lift_morphism"
+      {binding = [],
+       typ = [Logic.type_map term],
+       term = [term],
+       fact = [map f]}
   end
 
 fun import_function_data t ctxt =
diff -r 6db5fbc02436 -r 7068557b7c63 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/HOL/Tools/Function/function_elims.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -33,118 +33,121 @@
 
 local
 
-fun propagate_tac i thm =
-  let fun inspect eq = case eq of
-              Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
-                  if Logic.occs (Free x, t) then raise Match else true
-            | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
-                  if Logic.occs (Free x, t) then raise Match else false
-            | _ => raise Match;
-      fun mk_eq thm = (if inspect (prop_of thm) then
-                          [thm RS eq_reflection]
-                      else
-                          [Thm.symmetric (thm RS eq_reflection)])
-                      handle Match => [];
-      val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss
-               |> Simplifier.set_mksimps (K mk_eq)
+fun propagate_tac ctxt i =
+  let
+    fun inspect eq =
+      (case eq of
+        Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
+          if Logic.occs (Free x, t) then raise Match else true
+      | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
+          if Logic.occs (Free x, t) then raise Match else false
+      | _ => raise Match);
+    fun mk_eq thm =
+      (if inspect (prop_of thm) then [thm RS eq_reflection]
+       else [Thm.symmetric (thm RS eq_reflection)])
+      handle Match => [];
+    val simpset =
+      empty_simpset ctxt
+      |> Simplifier.set_mksimps (K mk_eq);
   in
-    asm_lr_simp_tac ss i thm
+    asm_lr_simp_tac simpset i
   end;
 
-val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}
-val boolE = @{thms HOL.TrueE HOL.FalseE}
-val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}
-val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}
+val eq_boolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+};
+val boolE = @{thms HOL.TrueE HOL.FalseE};
+val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+};
+val eq_bool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False};
 
 fun bool_subst_tac ctxt i =
-    REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i)
-    THEN REPEAT (dresolve_tac boolD i)
-    THEN REPEAT (eresolve_tac boolE i)
+  REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool i)
+  THEN REPEAT (dresolve_tac boolD i)
+  THEN REPEAT (eresolve_tac boolE i)
 
 fun mk_bool_elims ctxt elim =
-  let val tac = ALLGOALS (bool_subst_tac ctxt)
-      fun mk_bool_elim b =
-        elim
-        |> Thm.forall_elim b
-        |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1))
-        |> Tactic.rule_by_tactic ctxt tac
+  let
+    val tac = ALLGOALS (bool_subst_tac ctxt);
+    fun mk_bool_elim b =
+      elim
+      |> Thm.forall_elim b
+      |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eq_boolI 1))
+      |> Tactic.rule_by_tactic ctxt tac;
   in
-      map mk_bool_elim [@{cterm True}, @{cterm False}]
+    map mk_bool_elim [@{cterm True}, @{cterm False}]
   end;
 
 in
 
 fun mk_partial_elim_rules ctxt result =
   let
-      val thy = Proof_Context.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
+    val cert = cterm_of thy;
 
-      val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
-                          termination, domintros, ...} = result;
-      val n_fs = length fs;
+    val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
+    val n_fs = length fs;
 
-      fun mk_partial_elim_rule (idx,f) =
-        let fun mk_funeq 0 T (acc_vars, acc_lhs) =
-                let val y = Free("y",T) in
-                  (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T)
-                end
-              | mk_funeq n (Type(@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
-                let val xn = Free ("x" ^ Int.toString n,S) in
-                  mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn)
-                end
-              | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f]))
+    fun mk_partial_elim_rule (idx, f) =
+      let
+        fun mk_funeq 0 T (acc_vars, acc_lhs) =
+              let val y = Free("y", T)
+              in (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T) end
+          | mk_funeq n (Type (@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
+              let val xn = Free ("x" ^ Int.toString n, S)
+              in mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) end
+          | mk_funeq _ _ _ = raise TERM ("Not a function.", [f]);
 
-            val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl
-                                           |> HOLogic.dest_Trueprop
-                                           |> dest_funprop |> fst |> fst) = f)
-                                 psimps
+        val f_simps =
+          filter (fn r =>
+            (prop_of r |> Logic.strip_assums_concl
+              |> HOLogic.dest_Trueprop
+              |> dest_funprop |> fst |> fst) = f)
+            psimps;
 
-            val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl
-                                   |> HOLogic.dest_Trueprop
-                                   |> snd o fst o dest_funprop |> length;
-            val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f)
-            val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs)
-            val args = HOLogic.mk_tuple arg_vars;
-            val domT = R |> dest_Free |> snd |> hd o snd o dest_Type
-
-            val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
-
-            val cprop = cterm_of thy prop
+        val arity =
+          hd f_simps
+          |> prop_of
+          |> Logic.strip_assums_concl
+          |> HOLogic.dest_Trueprop
+          |> snd o fst o dest_funprop
+          |> length;
+        val (free_vars, prop, ranT) = mk_funeq arity (fastype_of f) ([], f);
+        val (rhs_var, arg_vars) = (case free_vars of x :: xs => (x, rev xs));
+        val args = HOLogic.mk_tuple arg_vars;
+        val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
 
-            val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
-            val asms_thms = map Thm.assume asms;
+        val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
+
+        val cprop = cert prop;
+
+        val asms = [cprop, cert (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
+        val asms_thms = map Thm.assume asms;
 
-            fun prep_subgoal i =
-              REPEAT (eresolve_tac @{thms Pair_inject} i)
-              THEN Method.insert_tac (case asms_thms of
-                                        thm::thms => (thm RS sym) :: thms) i
-              THEN propagate_tac i
-              THEN TRY
-                  ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
-              THEN bool_subst_tac ctxt i;
-
-          val tac = ALLGOALS prep_subgoal;
+        fun prep_subgoal_tac i =
+          REPEAT (eresolve_tac @{thms Pair_inject} i)
+          THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
+          THEN propagate_tac ctxt i
+          THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
+          THEN bool_subst_tac ctxt i;
 
-          val elim_stripped =
-                nth cases idx
-                |> Thm.forall_elim @{cterm "P::bool"}
-                |> Thm.forall_elim (cterm_of thy args)
-                |> Tactic.rule_by_tactic ctxt tac
-                |> fold_rev Thm.implies_intr asms
-                |> Thm.forall_intr (cterm_of thy rhs_var)
+      val elim_stripped =
+        nth cases idx
+        |> Thm.forall_elim @{cterm "P::bool"}
+        |> Thm.forall_elim (cert args)
+        |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
+        |> fold_rev Thm.implies_intr asms
+        |> Thm.forall_intr (cert rhs_var);
 
-          val bool_elims = (case ranT of
-                              Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
-                              | _ => []);
+      val bool_elims =
+        (case ranT of
+          Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
+        | _ => []);
 
-          fun unstrip rl =
-                rl  |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm
-                           (map (cterm_of thy) arg_vars))
-                    |> Thm.forall_intr @{cterm "P::bool"}
-
-      in
-        map unstrip (elim_stripped :: bool_elims)
-      end;
-
+      fun unstrip rl =
+        rl
+        |> fold_rev (Thm.forall_intr o cert) arg_vars
+        |> Thm.forall_intr @{cterm "P::bool"};
+    in
+      map unstrip (elim_stripped :: bool_elims)
+    end;
   in
     map_index mk_partial_elim_rule fs
   end;
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/Isar/class_declaration.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -64,7 +64,7 @@
 
     (* canonical interpretation *)
     val base_morph = inst_morph
-      $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class))
+      $> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class))
       $> Element.satisfy_morphism (the_list some_witn);
     val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);
 
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/Isar/element.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -391,7 +391,7 @@
     in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
 
 fun instT_morphism thy env =
-  Morphism.morphism
+  Morphism.morphism "Element.instT"
    {binding = [],
     typ = [instT_type env],
     term = [instT_term env],
@@ -434,7 +434,7 @@
     end;
 
 fun inst_morphism thy (envT, env) =
-  Morphism.morphism
+  Morphism.morphism "Element.inst"
    {binding = [],
     typ = [instT_type envT],
     term = [inst_term (envT, env)],
@@ -449,14 +449,14 @@
       NONE => I
     | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
 
-val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
+val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm;
 
 
 (* rewriting with equalities *)
 
 fun eq_morphism _ [] = NONE
   | eq_morphism thy thms =
-      SOME (Morphism.morphism
+      SOME (Morphism.morphism "Element.eq_morphism"
        {binding = [],
         typ = [],
         term = [Raw_Simplifier.rewrite_term thy thms []],
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/Isar/expression.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -171,7 +171,7 @@
 
 (* Instantiation morphism *)
 
-fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
+fun inst_morphism (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
   let
     (* parameters *)
     val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
@@ -192,7 +192,7 @@
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
-      Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
+      Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
   end;
 
 
@@ -299,7 +299,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
-    val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
+    val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst) ctxt;
   in (loc, morph) end;
 
 fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
@@ -368,7 +368,7 @@
         val insts' = insts @ [(loc, (prfx, inst''))];
         val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
-        val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
+        val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
         val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
       in (i + 1, insts', ctxt'') end;
 
@@ -513,7 +513,8 @@
     val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
     val export' =
-      Morphism.morphism {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
+      Morphism.morphism "Expression.prep_goal"
+        {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
   in ((propss, deps, export'), goal_ctxt) end;
 
 in
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/Isar/local_theory.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -189,7 +189,8 @@
 
 fun standard_morphism lthy ctxt =
   Proof_Context.norm_export_morphism lthy ctxt $>
-  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
+  Morphism.binding_morphism "Local_Theory.standard_binding"
+    (Name_Space.transform_binding (naming_of lthy));
 
 fun standard_form lthy ctxt x =
   Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/Isar/proof_context.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -762,7 +762,7 @@
 
 fun norm_export_morphism inner outer =
   export_morphism inner outer $>
-  Morphism.thm_morphism Goal.norm_result;
+  Morphism.thm_morphism "Proof_Context.norm_export" Goal.norm_result;
 
 
 
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/ROOT.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -328,6 +328,7 @@
 toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
+toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
 
 if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
 
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/assumption.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -121,6 +121,9 @@
     val thm = export false inner outer;
     val term = export_term inner outer;
     val typ = Logic.type_map term;
-  in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [map thm]} end;
+  in
+    Morphism.morphism "Assumption.export"
+      {binding = [], typ = [typ], term = [term], fact = [map thm]}
+  end;
 
 end;
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/morphism.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -16,23 +16,24 @@
 signature MORPHISM =
 sig
   include BASIC_MORPHISM
-  type 'a funs = ('a -> 'a) list
+  exception MORPHISM of string * exn
+  val pretty: morphism -> Pretty.T
   val binding: morphism -> binding -> binding
   val typ: morphism -> typ -> typ
   val term: morphism -> term -> term
   val fact: morphism -> thm list -> thm list
   val thm: morphism -> thm -> thm
   val cterm: morphism -> cterm -> cterm
-  val morphism:
-   {binding: binding funs,
-    typ: typ funs,
-    term: term funs,
-    fact: thm list funs} -> morphism
-  val binding_morphism: (binding -> binding) -> morphism
-  val typ_morphism: (typ -> typ) -> morphism
-  val term_morphism: (term -> term) -> morphism
-  val fact_morphism: (thm list -> thm list) -> morphism
-  val thm_morphism: (thm -> thm) -> morphism
+  val morphism: string ->
+   {binding: (binding -> binding) list,
+    typ: (typ -> typ) list,
+    term: (term -> term) list,
+    fact: (thm list -> thm list) list} -> morphism
+  val binding_morphism: string -> (binding -> binding) -> morphism
+  val typ_morphism: string -> (typ -> typ) -> morphism
+  val term_morphism: string -> (term -> term) -> morphism
+  val fact_morphism: string -> (thm list -> thm list) -> morphism
+  val thm_morphism: string -> (thm -> thm) -> morphism
   val transfer_morphism: theory -> morphism
   val identity: morphism
   val compose: morphism -> morphism -> morphism
@@ -43,17 +44,31 @@
 structure Morphism: MORPHISM =
 struct
 
-type 'a funs = ('a -> 'a) list;
-fun apply fs = fold_rev (fn f => fn x => f x) fs;
+(* named functions *)
+
+type 'a funs = (string * ('a -> 'a)) list;
+
+exception MORPHISM of string * exn;
+
+fun app (name, f) x = f x
+  handle exn => if Exn.is_interrupt exn then reraise exn else raise MORPHISM (name, exn);
+
+fun apply fs = fold_rev app fs;
+
+
+(* type morphism *)
 
 datatype morphism = Morphism of
- {binding: binding funs,
+ {names: string list,
+  binding: binding funs,
   typ: typ funs,
   term: term funs,
   fact: thm list funs};
 
 type declaration = morphism -> Context.generic -> Context.generic;
 
+fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
+
 fun binding (Morphism {binding, ...}) = apply binding;
 fun typ (Morphism {typ, ...}) = apply typ;
 fun term (Morphism {term, ...}) = apply term;
@@ -61,22 +76,36 @@
 val thm = singleton o fact;
 val cterm = Drule.cterm_rule o thm;
 
-val morphism = Morphism;
+
+fun morphism a {binding, typ, term, fact} =
+  Morphism {
+    names = if a = "" then [] else [a],
+    binding = map (pair a) binding,
+    typ = map (pair a) typ,
+    term = map (pair a) term,
+    fact = map (pair a) fact};
 
-fun binding_morphism binding = morphism {binding = [binding], typ = [], term = [], fact = []};
-fun typ_morphism typ = morphism {binding = [], typ = [typ], term = [], fact = []};
-fun term_morphism term = morphism {binding = [], typ = [], term = [term], fact = []};
-fun fact_morphism fact = morphism {binding = [], typ = [], term = [], fact = [fact]};
-fun thm_morphism thm = morphism {binding = [], typ = [], term = [], fact = [map thm]};
-val transfer_morphism = thm_morphism o Thm.transfer;
+fun binding_morphism a binding = morphism a {binding = [binding], typ = [], term = [], fact = []};
+fun typ_morphism a typ = morphism a {binding = [], typ = [typ], term = [], fact = []};
+fun term_morphism a term = morphism a {binding = [], typ = [], term = [term], fact = []};
+fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]};
+fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
+val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
 
-val identity = morphism {binding = [], typ = [], term = [], fact = []};
+val identity = morphism "" {binding = [], typ = [], term = [], fact = []};
+
+
+(* morphism combinators *)
 
 fun compose
-    (Morphism {binding = binding1, typ = typ1, term = term1, fact = fact1})
-    (Morphism {binding = binding2, typ = typ2, term = term2, fact = fact2}) =
-  morphism {binding = binding1 @ binding2, typ = typ1 @ typ2,
-    term = term1 @ term2, fact = fact1 @ fact2};
+    (Morphism {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1})
+    (Morphism {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2}) =
+  Morphism {
+    names = names1 @ names2,
+    binding = binding1 @ binding2,
+    typ = typ1 @ typ2,
+    term = term1 @ term2,
+    fact = fact1 @ fact2};
 
 fun phi1 $> phi2 = compose phi2 phi1;
 
diff -r 6db5fbc02436 -r 7068557b7c63 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Dec 14 07:26:45 2013 +0800
+++ b/src/Pure/variable.ML	Sat Dec 14 07:45:30 2013 +0800
@@ -461,7 +461,9 @@
     val fact = export inner outer;
     val term = singleton (export_terms inner outer);
     val typ = Logic.type_map term;
-  in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [fact]} end;
+  in
+    Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]}
+  end;