src/HOL/Import/replay.ML

 	    in
 		P.INST theta th thy'
 	    end
 	  | rp (PGen(prf,v)) thy =
 	    let
-		val _ = writeln "enter rp PGen"
-		val (thy',th) = rp' prf thy
-		val _ = writeln "replayed inner proof"
+		val (thy',th) = rp' prf thy
 		val p = P.GEN v th thy'
-		val _ = writeln "exit rp PGen"
 	    in
 		p
 	    end
 	  | rp (PGenAbs(prf,opt,vl)) thy =
 	    let

 						end
 					      | SOME th => (thy,th))
 				       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) => (writeln "Found theorem, no replay necessary!"; (thy',res))
+					    (thy',SOME res) => (thy',res)
 					  | (thy',NONE) => 
 					    if thyname' = thyname
 					    then
 						let
 						    val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")

 
 fun import_single_thm thyname int_thms thmname thy =
     let
 	fun replay_fact (thmname,thy) =
 	    let
-		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 _ = writeln ("Replaying "^thmname^" ...")
 		val p = fst (replay_proof int_thms thyname thmname prf thy)
-		val _ = writeln ("exit replay_fact")
 	    in
 		p
 	    end
     in
 	replay_fact (thmname,thy)

 
 fun import_thms thyname int_thms thmnames thy =
     let
 	fun replay_fact (thy,thmname) =
 	    let
-		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 _ = set_disk_info_of prf thyname thmname
+                val _ = writeln ("Replaying "^thmname^" ...")
 		val p = fst (replay_proof int_thms thyname thmname prf thy)
-		val _ = writeln ("exit replay_fact")
 	    in
 		p
 	    end
 	val res_thy = Library.foldl replay_fact (thy,thmnames)
     in

 fun import_thm thyname thmname thy =
     let
 	val int_thms = fst (setup_int_thms thyname thy)
 	fun replay_fact (thmname,thy) =
 	    let
-		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 _ = set_disk_info_of prf thyname thmname 	    
+                val _ = writeln ("Replaying "^thmname^" ...")
 		val p = fst (replay_proof int_thms thyname thmname prf thy)
-		val _ = writeln ("exit replay_fact")	    
 	    in 
 		p
 	    end
     in
 	replay_fact (thmname,thy)