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/Pure/Isar/interpretation.ML
changeset 69058 f4fb93197670
parent 69050 812e60d15172
child 69699 82f57315cade 
--- a/src/Pure/Isar/interpretation.ML	Mon Sep 24 19:34:14 2018 +0200
+++ b/src/Pure/Isar/interpretation.ML	Mon Sep 24 19:43:20 2018 +0200
@@ -115,7 +115,7 @@
         (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
     fun register (dep, eqns) ctxt =
       ctxt |> add_registration
-        {dep = dep,
+        {inst = dep,
           mixin =
             Option.map (rpair true)
               (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
isabelle