--- a/Nominal/nominal_function_common.ML	Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_function_common.ML	Sun Dec 15 15:14:40 2013 +1100
@@ -76,8 +76,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 =