changeset 26481 | 92e901171cc8 |
parent 22846 | fb79144af9a3 |
child 26928 | ca87aff1ad2d |
--- a/src/HOL/Import/hol4rews.ML Sat Mar 29 19:14:00 2008 +0100 +++ b/src/HOL/Import/hol4rews.ML Sat Mar 29 19:14:03 2008 +0100 @@ -390,7 +390,7 @@ val thm2 = standard thm1; in thy - |> PureThy.store_thm ((bthm, thm2), []) + |> PureThy.store_thm (bthm, thm2) |> snd |> add_hol4_theorem bthy bthm hth end;