| changeset 54740 | 91f54d386680 |
| parent 53673 | bcfd16f65014 |
| child 54742 | 7a86358a3c0b |
--- a/src/Pure/Isar/proof_context.ML Fri Dec 13 14:58:47 2013 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Dec 13 20:20:15 2013 +0100 @@ -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;