Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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))
isabelle