src/HOL/Import/replay.ML
changeset 17322 781abf7011e6
parent 15574 b1d1b5bfc464
child 17440 df77edc4f5d0
     1.1 --- a/src/HOL/Import/replay.ML	Mon Sep 12 12:11:17 2005 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Mon Sep 12 15:52:00 2005 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4  	       | (thy',NONE) => 
     1.5  		 if seg = thyname
     1.6  		 then P.new_definition seg name rhs thy'
     1.7 -		 else raise ERR "replay_proof" "Too late for term definition")
     1.8 +		 else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
     1.9  	  | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    1.10  	  | rp (PSpec(prf,tm)) thy =
    1.11  	    let
    1.12 @@ -234,6 +234,7 @@
    1.13  						    val (f_opt,prf) = import_proof thyname' thmname thy'
    1.14  						    val prf = prf thy'
    1.15  						    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
    1.16 +                                                    val _ = writeln ("Successfully finished replaying "^thmname^" !")
    1.17  						in
    1.18  						    case content_of prf of
    1.19  							PTmSpec _ => (thy',th)