1.1 --- a/src/HOL/Import/import.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Import/import.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4              val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
     1.5              val thm = snd (ProofKernel.to_isa_thm hol4thm)
     1.6              val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
     1.7 -            val thm = equal_elim rew thm
     1.8 +            val thm = Thm.equal_elim rew thm
     1.9              val prew = ProofKernel.rewrite_hol4_term prem thy
    1.10              val prem' = #2 (Logic.dest_equals (prop_of prew))
    1.11              val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
    1.12 @@ -53,7 +53,7 @@
    1.13                      val _ = if prem' aconv (prop_of thm)
    1.14                              then message "import: Terms match up"
    1.15                              else message "import: Terms DO NOT match up"
    1.16 -                    val thm' = equal_elim (symmetric prew) thm
    1.17 +                    val thm' = Thm.equal_elim (Thm.symmetric prew) thm
    1.18                      val res = Thm.bicompose true (false,thm',0) 1 th
    1.19                  in
    1.20                      res