diff -r 25e9e7f527b4 -r f599ac41e7f5 src/Tools/interpretation_with_defs.ML
--- a/src/Tools/interpretation_with_defs.ML	Fri Oct 28 15:38:41 2011 +0200
+++ b/src/Tools/interpretation_with_defs.ML	Fri Oct 28 17:15:52 2011 +0200
@@ -30,7 +30,7 @@
     |-> (fn eqns => fold (fn ((dep, morph), wits) =>
       fn context =>
         Locale.add_registration (dep, morph $> Element.satisfy_morphism
-            (map (Element.morph_witness export') wits))
+            (map (Element.transform_witness export') wits))
           (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
             Option.map (rpair true))
           export context) (deps ~~ witss))