1.1 --- a/src/HOL/Import/hol4rews.ML	Sat Mar 29 19:14:00 2008 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Mar 29 19:14:03 2008 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4          val thm2 = standard thm1;
     1.5        in
     1.6          thy
     1.7 -        |> PureThy.store_thm ((bthm, thm2), [])
     1.8 +        |> PureThy.store_thm (bthm, thm2)
     1.9          |> snd
    1.10          |> add_hol4_theorem bthy bthm hth
    1.11        end;