# HG changeset patch
# User wenzelm
# Date 1129651174 -7200
# Node ID 75d3120779419d0e8e5abe2bbefeb0d38503a586
# Parent  5f44c71c4ca4872b20a2d70a81fd8bcf6646ea60
ObjectLogic.atomize_cterm;

diff -r 5f44c71c4ca4 -r 75d312077941 src/Pure/Isar/locale.ML
--- 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 =>