src/HOL/Import/replay.ML
changeset 46201 afdc69f5156e
parent 43918 6ca79a354c51
child 46784 71d1ed1ed8d8
     1.1 --- a/src/HOL/Import/replay.ML	Thu Jan 12 23:29:03 2012 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Jan 13 11:50:28 2012 +0100
     1.3 @@ -229,7 +229,7 @@
     1.4                                              then
     1.5                                                  let
     1.6                                                      val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
     1.7 -                                                    val (f_opt,prf) = import_proof thyname' thmname thy'
     1.8 +                                                    val (_, prf) = import_proof thyname' thmname thy'
     1.9                                                      val prf = prf thy'
    1.10                                                      val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
    1.11                                                      val _ = writeln ("Successfully finished replaying "^thmname^" !")