src/HOL/Import/replay.ML
changeset 17594 98be710dabc4
parent 17592 ece268908438
child 17959 8db36a108213
     1.1 --- a/src/HOL/Import/replay.ML	Fri Sep 23 09:00:19 2005 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Sep 23 10:01:14 2005 +0200
     1.3 @@ -77,11 +77,8 @@
     1.4  	    end
     1.5  	  | rp (PGen(prf,v)) thy =
     1.6  	    let
     1.7 -		val _ = writeln "enter rp PGen"
     1.8  		val (thy',th) = rp' prf thy
     1.9 -		val _ = writeln "replayed inner proof"
    1.10  		val p = P.GEN v th thy'
    1.11 -		val _ = writeln "exit rp PGen"
    1.12  	    in
    1.13  		p
    1.14  	    end
    1.15 @@ -229,7 +226,7 @@
    1.16  				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
    1.17  				     | NONE => 
    1.18  				       (case P.get_thm thyname' thmname thy of
    1.19 -					    (thy',SOME res) => (writeln "Found theorem, no replay necessary!"; (thy',res))
    1.20 +					    (thy',SOME res) => (thy',res)
    1.21  					  | (thy',NONE) => 
    1.22  					    if thyname' = thyname
    1.23  					    then
    1.24 @@ -304,13 +301,10 @@
    1.25      let
    1.26  	fun replay_fact (thmname,thy) =
    1.27  	    let
    1.28 -		val _ = writeln ("import_single_thm: Replaying " ^ thmname)
    1.29  		val prf = mk_proof PDisk
    1.30 -		val _ = writeln ("Made proof.")
    1.31  		val _ = set_disk_info_of prf thyname thmname
    1.32 -		val _ = writeln ("set disk info")	    
    1.33 +                val _ = writeln ("Replaying "^thmname^" ...")
    1.34  		val p = fst (replay_proof int_thms thyname thmname prf thy)
    1.35 -		val _ = writeln ("exit replay_fact")
    1.36  	    in
    1.37  		p
    1.38  	    end
    1.39 @@ -322,13 +316,10 @@
    1.40      let
    1.41  	fun replay_fact (thy,thmname) =
    1.42  	    let
    1.43 -		val _ = writeln ("import_thms: Replaying " ^ thmname)
    1.44  		val prf = mk_proof PDisk	
    1.45 -		val _ = writeln ("Made proof.")
    1.46 -		val _ = set_disk_info_of prf thyname thmname	
    1.47 -		val _ = writeln ("set disk info")	    
    1.48 +		val _ = set_disk_info_of prf thyname thmname
    1.49 +                val _ = writeln ("Replaying "^thmname^" ...")
    1.50  		val p = fst (replay_proof int_thms thyname thmname prf thy)
    1.51 -		val _ = writeln ("exit replay_fact")
    1.52  	    in
    1.53  		p
    1.54  	    end
    1.55 @@ -342,13 +333,10 @@
    1.56  	val int_thms = fst (setup_int_thms thyname thy)
    1.57  	fun replay_fact (thmname,thy) =
    1.58  	    let
    1.59 -		val _ = writeln ("import_thm: Replaying " ^ thmname)
    1.60  		val prf = mk_proof PDisk	
    1.61 -		val _ = writeln ("Made proof.")
    1.62 -		val _ = set_disk_info_of prf thyname thmname 
    1.63 -		val _ = writeln ("set disk info")	    
    1.64 +		val _ = set_disk_info_of prf thyname thmname 	    
    1.65 +                val _ = writeln ("Replaying "^thmname^" ...")
    1.66  		val p = fst (replay_proof int_thms thyname thmname prf thy)
    1.67 -		val _ = writeln ("exit replay_fact")	    
    1.68  	    in 
    1.69  		p
    1.70  	    end