| changeset 25026 | ecdc1733d3cc |
| parent 25021 | 8f00edb993bd |
| child 25104 | 26b9a7db3386 |
--- 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) $>