# HG changeset patch
# User wenzelm
# Date 1138144894 -3600
# Node ID fdc5379fd359eee041dd85ae02bbca5fdacc7761
# Parent  becdbf57eeb8b5218890234f01b4b1ea9f85e796
ObjectLogic.atomize_cterm;

diff -r becdbf57eeb8 -r fdc5379fd359 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Wed Jan 25 00:21:32 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Wed Jan 25 00:21:34 2006 +0100
@@ -126,7 +126,7 @@
         fun typ_equiv t u = Sign.typ_instance thy (t,u) andalso Sign.typ_instance thy (u,t);
 
         val rew_imps = alt_props |>
-          map (ObjectLogic.atomize_cterm thy o Thm.read_cterm thy o rpair Term.propT o snd)
+          map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd)
         val props' = rew_imps |>
           map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of)