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