# HG changeset patch
# User wenzelm
# Date 1011297940 -3600
# Node ID 1f54c65fca5db34c780fb4d000b79e4b4d7e12e0
# Parent  3be853cf19cf1b30e818699bc037bcef794a6ead
ObjectLogic.atomize_term replaces ObjectLogic.atomize_cterm;

diff -r 3be853cf19cf -r 1f54c65fca5d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jan 17 21:04:48 2002 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Jan 17 21:05:40 2002 +0100
@@ -731,7 +731,7 @@
       if null pred_ts then Pretty.str ""
       else
         Library.foldr1 Logic.mk_conjunction pred_ts
-        |> Thm.cterm_of sg |> ObjectLogic.atomize_cterm |> Thm.term_of
+        |> ObjectLogic.atomize_term sg
         |> curry Term.list_abs_free pred_xs
         |> prt_term;
   in