changeset 17901 | 75d312077941 |
parent 17856 | 0551978bfda5 |
child 17973 | ef2c44da2f68 |
--- a/src/Pure/Isar/locale.ML Tue Oct 18 17:59:33 2005 +0200 +++ b/src/Pure/Isar/locale.ML Tue Oct 18 17:59:34 2005 +0200 @@ -1866,7 +1866,7 @@ val bodyT = Term.fastype_of body; in if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) - else (body, bodyT, ObjectLogic.atomize_rule thy (Thm.cterm_of thy t)) + else (body, bodyT, ObjectLogic.atomize_cterm thy (Thm.cterm_of thy t)) end; fun aprop_tr' n c = (c, fn args =>