--- a/src/HOL/Import/replay.ML Fri Sep 23 00:11:10 2005 +0200
+++ b/src/HOL/Import/replay.ML Fri Sep 23 00:52:13 2005 +0200
@@ -77,9 +77,13 @@
end
| rp (PGen(prf,v)) thy =
let
+ val _ = writeln "enter rp PGen"
val (thy',th) = rp' prf thy
+ val _ = writeln "replayed inner proof"
+ val p = P.GEN v th thy'
+ val _ = writeln "exit rp PGen"
in
- P.GEN v th thy'
+ p
end
| rp (PGenAbs(prf,opt,vl)) thy =
let
@@ -225,7 +229,7 @@
else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
| NONE =>
(case P.get_thm thyname' thmname thy of
- (thy',SOME res) => (thy',res)
+ (thy',SOME res) => (writeln "Found theorem, no replay necessary!"; (thy',res))
| (thy',NONE) =>
if thyname' = thyname
then
@@ -300,11 +304,15 @@
let
fun replay_fact (thmname,thy) =
let
- val _ = writeln ("Replaying " ^ thmname)
+ val _ = writeln ("import_single_thm: Replaying " ^ thmname)
val prf = mk_proof PDisk
+ val _ = writeln ("Made proof.")
val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("set disk info")
+ val p = fst (replay_proof int_thms thyname thmname prf thy)
+ val _ = writeln ("exit replay_fact")
in
- fst (replay_proof int_thms thyname thmname prf thy)
+ p
end
in
replay_fact (thmname,thy)
@@ -314,11 +322,15 @@
let
fun replay_fact (thy,thmname) =
let
- val _ = writeln ("Replaying " ^ thmname)
- val prf = mk_proof PDisk
- val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("import_thms: Replaying " ^ thmname)
+ val prf = mk_proof PDisk
+ val _ = writeln ("Made proof.")
+ val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("set disk info")
+ val p = fst (replay_proof int_thms thyname thmname prf thy)
+ val _ = writeln ("exit replay_fact")
in
- fst (replay_proof int_thms thyname thmname prf thy)
+ p
end
val res_thy = Library.foldl replay_fact (thy,thmnames)
in
@@ -330,11 +342,15 @@
val int_thms = fst (setup_int_thms thyname thy)
fun replay_fact (thmname,thy) =
let
- val _ = writeln ("Replaying " ^ thmname)
- val prf = mk_proof PDisk
- val _ = set_disk_info_of prf thyname thmname
- in
- fst (replay_proof int_thms thyname thmname prf thy)
+ val _ = writeln ("import_thm: Replaying " ^ thmname)
+ val prf = mk_proof PDisk
+ val _ = writeln ("Made proof.")
+ val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("set disk info")
+ val p = fst (replay_proof int_thms thyname thmname prf thy)
+ val _ = writeln ("exit replay_fact")
+ in
+ p
end
in
replay_fact (thmname,thy)