# HG changeset patch
# User haftmann
# Date 1330804892 -3600
# Node ID 71d1ed1ed8d887bc211a3f22093f2aa8fe462567
# Parent  3e89a5cab8d778a24f459935b6a788eedc6c678c
dropped dead code

diff -r 3e89a5cab8d7 -r 71d1ed1ed8d8 src/HOL/Import/hol4rews.ML
--- 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 ^ "\"")
diff -r 3e89a5cab8d7 -r 71d1ed1ed8d8 src/HOL/Import/replay.ML
--- 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