Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 14 Oct 2007 00:18:07 +0200
changeset 25026 ecdc1733d3cc
parent 25025 17c845095a47
child 25027 44b60657f54f
tuned;
src/Pure/Isar/local_theory.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/local_theory.ML	Sun Oct 14 00:18:06 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sun Oct 14 00:18:07 2007 +0200
@@ -159,7 +159,7 @@
 val declaration = operation1 #declaration;
 val target_naming = operation #target_naming;
 
-fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd;
+fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> the_single;
 
 fun target_morphism lthy =
   ProofContext.export_morphism lthy (target_of lthy) $>
isabelle