dropped dead code

--- a/src/HOL/Import/hol4rews.ML	Sat Mar 03 21:01:23 2012 +0100
+++ b/src/HOL/Import/hol4rews.ML	Sat Mar 03 21:01:32 2012 +0100
@@ -323,7 +323,7 @@
         val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
         val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
                (* FIXME avoid handle x *)
-               handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
+               handle x => let val (_, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
                       warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
         val upd_thy = HOL4TypeMaps.put newmaps thy
     in
@@ -513,7 +513,7 @@
         val _ = if null constmaps
                 then ()
                 else out "const_maps"
-        val _ = app (fn (hol,(internal,isa,opt_ty)) =>
+        val _ = app (fn (hol,(_,isa,opt_ty)) =>
                         (out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
                          case opt_ty of
                              SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")

--- a/src/HOL/Import/replay.ML	Sat Mar 03 21:01:23 2012 +0100
+++ b/src/HOL/Import/replay.ML	Sat Mar 03 21:01:32 2012 +0100
@@ -59,7 +59,7 @@
                  if seg = thyname
                  then ProofKernel.new_definition seg name rhs thy'
                  else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
-          | rp (POracle(tg,asl,c)) thy = (*ProofKernel.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
+          | rp (POracle _) thy = NY "ORACLE"
           | rp (PSpec(prf,tm)) thy =
             let
                 val (thy',th) = rp' prf thy