1.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -977,7 +977,7 @@
     1.4  
     1.5  fun uniq_compose m th i st =
     1.6      let
     1.7 -        val res = bicompose false (false,th,m) i st
     1.8 +        val res = Thm.bicompose false (false,th,m) i st
     1.9      in
    1.10          case Seq.pull res of
    1.11              SOME (th,rest) => (case Seq.pull rest of
    1.12 @@ -1065,14 +1065,12 @@
    1.13          res
    1.14      end
    1.15  
    1.16 -val permute_prems = Thm.permute_prems
    1.17 -
    1.18  fun rearrange sg tm th =
    1.19      let
    1.20          val tm' = Envir.beta_eta_contract tm
    1.21 -        fun find []      n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
    1.22 +        fun find []      n = Thm.permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
    1.23            | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
    1.24 -                             then permute_prems n 1 th
    1.25 +                             then Thm.permute_prems n 1 th
    1.26                               else find ps (n+1)
    1.27      in
    1.28          find (prems_of th) 0
    1.29 @@ -1193,7 +1191,7 @@
    1.30  fun if_debug f x = if !debug then f x else ()
    1.31  val message = if_debug writeln
    1.32  
    1.33 -val conjE_helper = permute_prems 0 1 conjE
    1.34 +val conjE_helper = Thm.permute_prems 0 1 conjE
    1.35  
    1.36  fun get_hol4_thm thyname thmname thy =
    1.37      case get_hol4_theorem thyname thmname thy of