src/Pure/Isar/expression.ML
changeset 42440 5e7a7343ab11
parent 42381 309ec68442c6
child 42482 42c7ef050bc3
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Apr 20 22:57:29 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Apr 21 12:56:27 2011 +0200
     1.3 @@ -725,7 +725,7 @@
     1.4    | assumes_to_notes e axms = (e, axms);
     1.5  
     1.6  fun defines_to_notes thy (Defines defs) =
     1.7 -      Notes (Thm.definitionK, map (fn (a, (def, _)) =>
     1.8 +      Notes ("", map (fn (a, (def, _)) =>
     1.9          (a, [([Assumption.assume (cterm_of thy def)],
    1.10            [(Attrib.internal o K) Locale.witness_add])])) defs)
    1.11    | defines_to_notes _ e = e;