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