src/HOL/Import/replay.ML
changeset 17592 ece268908438
parent 17440 df77edc4f5d0
child 17594 98be710dabc4
     1.1 --- a/src/HOL/Import/replay.ML	Fri Sep 23 00:11:10 2005 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Sep 23 00:52:13 2005 +0200
     1.3 @@ -77,9 +77,13 @@
     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.GEN v th thy'
    1.14 +		p
    1.15  	    end
    1.16  	  | rp (PGenAbs(prf,opt,vl)) thy =
    1.17  	    let
    1.18 @@ -225,7 +229,7 @@
    1.19  				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
    1.20  				     | NONE => 
    1.21  				       (case P.get_thm thyname' thmname thy of
    1.22 -					    (thy',SOME res) => (thy',res)
    1.23 +					    (thy',SOME res) => (writeln "Found theorem, no replay necessary!"; (thy',res))
    1.24  					  | (thy',NONE) => 
    1.25  					    if thyname' = thyname
    1.26  					    then
    1.27 @@ -300,11 +304,15 @@
    1.28      let
    1.29  	fun replay_fact (thmname,thy) =
    1.30  	    let
    1.31 -		val _ = writeln ("Replaying " ^ thmname)
    1.32 +		val _ = writeln ("import_single_thm: Replaying " ^ thmname)
    1.33  		val prf = mk_proof PDisk
    1.34 +		val _ = writeln ("Made proof.")
    1.35  		val _ = set_disk_info_of prf thyname thmname
    1.36 +		val _ = writeln ("set disk info")	    
    1.37 +		val p = fst (replay_proof int_thms thyname thmname prf thy)
    1.38 +		val _ = writeln ("exit replay_fact")
    1.39  	    in
    1.40 -		fst (replay_proof int_thms thyname thmname prf thy)
    1.41 +		p
    1.42  	    end
    1.43      in
    1.44  	replay_fact (thmname,thy)
    1.45 @@ -314,11 +322,15 @@
    1.46      let
    1.47  	fun replay_fact (thy,thmname) =
    1.48  	    let
    1.49 -		val _ = writeln ("Replaying " ^ thmname)
    1.50 -		val prf = mk_proof PDisk
    1.51 -		val _ = set_disk_info_of prf thyname thmname
    1.52 +		val _ = writeln ("import_thms: Replaying " ^ thmname)
    1.53 +		val prf = mk_proof PDisk	
    1.54 +		val _ = writeln ("Made proof.")
    1.55 +		val _ = set_disk_info_of prf thyname thmname	
    1.56 +		val _ = writeln ("set disk info")	    
    1.57 +		val p = fst (replay_proof int_thms thyname thmname prf thy)
    1.58 +		val _ = writeln ("exit replay_fact")
    1.59  	    in
    1.60 -		fst (replay_proof int_thms thyname thmname prf thy)
    1.61 +		p
    1.62  	    end
    1.63  	val res_thy = Library.foldl replay_fact (thy,thmnames)
    1.64      in
    1.65 @@ -330,11 +342,15 @@
    1.66  	val int_thms = fst (setup_int_thms thyname thy)
    1.67  	fun replay_fact (thmname,thy) =
    1.68  	    let
    1.69 -		val _ = writeln ("Replaying " ^ thmname)
    1.70 -		val prf = mk_proof PDisk
    1.71 -		val _ = set_disk_info_of prf thyname thmname
    1.72 -	    in
    1.73 -		fst (replay_proof int_thms thyname thmname prf thy)
    1.74 +		val _ = writeln ("import_thm: Replaying " ^ thmname)
    1.75 +		val prf = mk_proof PDisk	
    1.76 +		val _ = writeln ("Made proof.")
    1.77 +		val _ = set_disk_info_of prf thyname thmname 
    1.78 +		val _ = writeln ("set disk info")	    
    1.79 +		val p = fst (replay_proof int_thms thyname thmname prf thy)
    1.80 +		val _ = writeln ("exit replay_fact")	    
    1.81 +	    in 
    1.82 +		p
    1.83  	    end
    1.84      in
    1.85  	replay_fact (thmname,thy)