changeset 22902 | ac833b4bb7ee |
parent 22709 | 9ab51bac6287 |
child 23591 | d32a85385e17 |
--- a/src/HOL/Tools/specification_package.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/HOL/Tools/specification_package.ML Thu May 10 00:39:48 2007 +0200 @@ -123,7 +123,7 @@ val rew_imps = alt_props |> 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) + map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) fun proc_single prop = let