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/expression.ML
changeset 61336 fa4ebbd350ae
parent 61082 42c2698d2273
child 61669 27ca6147e3b3 
--- a/src/Pure/Isar/expression.ML	Tue Oct 06 11:29:00 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Oct 06 13:31:44 2015 +0200
@@ -888,7 +888,7 @@
     val facts = map2 (fn attrs => fn eqn =>
       (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
     val (eqns', ctxt') = ctxt
-      |> note Thm.lemmaK facts
+      |> note Thm.theoremK facts
       |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
     val dep_morphs =
       map2 (fn (dep, morph) => fn wits =>
isabelle