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/locale.ML
changeset 30777 9960ff945c52
parent 30775 71f777103225
child 31988 801aabf9f376 
--- a/src/Pure/Isar/locale.ML	Sun Mar 29 17:47:58 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Mar 29 18:06:14 2009 +0200
@@ -370,7 +370,7 @@
 
 fun add_thmss loc kind args ctxt =
   let
-    val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
+    val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
     val ctxt'' = ctxt' |> ProofContext.theory (
       (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
         #>
isabelle