# HG changeset patch
# User wenzelm
# Date 1192313887 -7200
# Node ID ecdc1733d3ccbd9f50e538406fe86f96ecde8902
# Parent  17c845095a4710cac4fce831c5a9e6b0af950efb
tuned;

diff -r 17c845095a47 -r ecdc1733d3cc src/Pure/Isar/local_theory.ML
--- 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) $>