src/HOL/Tools/specification_package.ML
changeset 18776 fdc5379fd359
parent 18729 216e31270509
child 18799 f137c5e971f5
--- 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)