src/HOL/Import/replay.ML
changeset 17959 8db36a108213
parent 17594 98be710dabc4
child 19064 bf19cc5a7899
     1.1 --- a/src/HOL/Import/replay.ML	Fri Oct 21 18:14:37 2005 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Oct 21 18:14:38 2005 +0200
     1.3 @@ -270,7 +270,7 @@
     1.4  		  | _ => rp pc thy
     1.5  	    end
     1.6      in
     1.7 -	rp' prf thy handle e => (writeln "Exception in replay_proof"; print_exn e)
     1.8 +	rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
     1.9      end
    1.10  
    1.11  fun setup_int_thms thyname thy =
    1.12 @@ -344,4 +344,4 @@
    1.13  	replay_fact (thmname,thy)
    1.14      end
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end