ObjectLogic.atomize_cterm;

--- 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 =>