src/Tools/interpretation_with_defs.ML
changeset 45290 f599ac41e7f5
parent 42361 23f352990944
child 46858 05f30c796f95
--- 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))