tuned;
authorwenzelm
Sun Oct 14 00:18:07 2007 +0200 (2007-10-14 ago)
changeset 25026ecdc1733d3cc
parent 25025 17c845095a47
child 25027 44b60657f54f
tuned;
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sun Oct 14 00:18:06 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sun Oct 14 00:18:07 2007 +0200
     1.3 @@ -159,7 +159,7 @@
     1.4  val declaration = operation1 #declaration;
     1.5  val target_naming = operation #target_naming;
     1.6  
     1.7 -fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd;
     1.8 +fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> the_single;
     1.9  
    1.10  fun target_morphism lthy =
    1.11    ProofContext.export_morphism lthy (target_of lthy) $>