src/HOL/Import/replay.ML
changeset 32960 69916a850301
parent 31723 f5cafe803b55
child 32966 5b21661fe618
     1.1 --- a/src/HOL/Import/replay.ML	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Import/replay.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Sebastian Skalberg (TU Muenchen)
     1.7  *)
     1.8  
     1.9 @@ -17,406 +16,406 @@
    1.10  
    1.11  fun replay_proof int_thms thyname thmname prf thy =
    1.12      let
    1.13 -	val _ = ImportRecorder.start_replay_proof thyname thmname 
    1.14 -	fun rp (PRefl tm) thy = P.REFL tm thy
    1.15 -	  | rp (PInstT(p,lambda)) thy =
    1.16 -	    let
    1.17 -		val (thy',th) = rp' p thy
    1.18 -	    in
    1.19 -		P.INST_TYPE lambda th thy'
    1.20 -	    end
    1.21 -	  | rp (PSubst(prfs,ctxt,prf)) thy =
    1.22 -	    let
    1.23 -		val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
    1.24 -					   let
    1.25 -					       val (thy',th) = rp' p thy
    1.26 -					   in
    1.27 -					       (thy',th::ths)
    1.28 -					   end) prfs (thy,[])
    1.29 -		val (thy'',th) = rp' prf thy'
    1.30 -	    in
    1.31 -		P.SUBST ths ctxt th thy''
    1.32 -	    end
    1.33 -	  | rp (PAbs(prf,v)) thy =
    1.34 -	    let
    1.35 -		val (thy',th) = rp' prf thy
    1.36 -	    in
    1.37 -		P.ABS v th thy'
    1.38 -	    end
    1.39 -	  | rp (PDisch(prf,tm)) thy =
    1.40 -	    let
    1.41 -		val (thy',th) = rp' prf thy
    1.42 -	    in
    1.43 -		P.DISCH tm th thy'
    1.44 -	    end
    1.45 -	  | rp (PMp(prf1,prf2)) thy =
    1.46 -	    let
    1.47 -		val (thy1,th1) = rp' prf1 thy
    1.48 -		val (thy2,th2) = rp' prf2 thy1
    1.49 -	    in
    1.50 -		P.MP th1 th2 thy2
    1.51 -	    end
    1.52 -	  | rp (PHyp tm) thy = P.ASSUME tm thy
    1.53 -	  | rp (PDef(seg,name,rhs)) thy =
    1.54 -	    (case P.get_def seg name rhs thy of
    1.55 -		 (thy',SOME res) => (thy',res)
    1.56 -	       | (thy',NONE) => 
    1.57 -		 if seg = thyname
    1.58 -		 then P.new_definition seg name rhs thy'
    1.59 -		 else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
    1.60 -	  | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
    1.61 -	  | rp (PSpec(prf,tm)) thy =
    1.62 -	    let
    1.63 -		val (thy',th) = rp' prf thy
    1.64 -	    in
    1.65 -		P.SPEC tm th thy'
    1.66 -	    end
    1.67 -	  | rp (PInst(prf,theta)) thy =
    1.68 -	    let
    1.69 -		val (thy',th) = rp' prf thy
    1.70 -	    in
    1.71 -		P.INST theta th thy'
    1.72 -	    end
    1.73 -	  | rp (PGen(prf,v)) thy =
    1.74 -	    let
    1.75 -		val (thy',th) = rp' prf thy
    1.76 -		val p = P.GEN v th thy'
    1.77 -	    in
    1.78 -		p
    1.79 -	    end
    1.80 -	  | rp (PGenAbs(prf,opt,vl)) thy =
    1.81 -	    let
    1.82 -		val (thy',th) = rp' prf thy
    1.83 -	    in
    1.84 -		P.GEN_ABS opt vl th thy'
    1.85 -	    end
    1.86 -	  | rp (PImpAS(prf1,prf2)) thy =
    1.87 -	    let
    1.88 -		val (thy1,th1) = rp' prf1 thy
    1.89 -		val (thy2,th2) = rp' prf2 thy1
    1.90 -	    in
    1.91 -		P.IMP_ANTISYM th1 th2 thy2
    1.92 -	    end
    1.93 -	  | rp (PSym prf) thy =
    1.94 -	    let
    1.95 -		val (thy1,th) = rp' prf thy
    1.96 -	    in
    1.97 -		P.SYM th thy1
    1.98 -	    end
    1.99 -	  | rp (PTrans(prf1,prf2)) thy =
   1.100 -	    let
   1.101 -		val (thy1,th1) = rp' prf1 thy
   1.102 -		val (thy2,th2) = rp' prf2 thy1
   1.103 -	    in
   1.104 -		P.TRANS th1 th2 thy2
   1.105 -	    end
   1.106 -	  | rp (PComb(prf1,prf2)) thy =
   1.107 -	    let
   1.108 -		val (thy1,th1) = rp' prf1 thy
   1.109 -		val (thy2,th2) = rp' prf2 thy1
   1.110 -	    in
   1.111 -		P.COMB th1 th2 thy2
   1.112 -	    end
   1.113 -	  | rp (PEqMp(prf1,prf2)) thy =
   1.114 -	    let
   1.115 -		val (thy1,th1) = rp' prf1 thy
   1.116 -		val (thy2,th2) = rp' prf2 thy1
   1.117 -	    in
   1.118 -		P.EQ_MP th1 th2 thy2
   1.119 -	    end
   1.120 -	  | rp (PEqImp prf) thy =
   1.121 -	    let
   1.122 -		val (thy',th) = rp' prf thy
   1.123 -	    in
   1.124 -		P.EQ_IMP_RULE th thy'
   1.125 -	    end
   1.126 -	  | rp (PExists(prf,ex,wit)) thy =
   1.127 -	    let
   1.128 -		val (thy',th) = rp' prf thy
   1.129 -	    in
   1.130 -		P.EXISTS ex wit th thy'
   1.131 -	    end
   1.132 -	  | rp (PChoose(v,prf1,prf2)) thy =
   1.133 -	    let
   1.134 -		val (thy1,th1) = rp' prf1 thy
   1.135 -		val (thy2,th2) = rp' prf2 thy1
   1.136 -	    in
   1.137 -		P.CHOOSE v th1 th2 thy2
   1.138 -	    end
   1.139 -	  | rp (PConj(prf1,prf2)) thy =
   1.140 -	    let
   1.141 -		val (thy1,th1) = rp' prf1 thy
   1.142 -		val (thy2,th2) = rp' prf2 thy1
   1.143 -	    in
   1.144 -		P.CONJ th1 th2 thy2
   1.145 -	    end
   1.146 -	  | rp (PConjunct1 prf) thy =
   1.147 -	    let
   1.148 -		val (thy',th) = rp' prf thy
   1.149 -	    in
   1.150 -		P.CONJUNCT1 th thy'
   1.151 -	    end
   1.152 -	  | rp (PConjunct2 prf) thy =
   1.153 -	    let
   1.154 -		val (thy',th) = rp' prf thy
   1.155 -	    in
   1.156 -		P.CONJUNCT2 th thy'
   1.157 -	    end
   1.158 -	  | rp (PDisj1(prf,tm)) thy =
   1.159 -	    let
   1.160 -		val (thy',th) = rp' prf thy
   1.161 -	    in
   1.162 -		P.DISJ1 th tm thy'
   1.163 -	    end
   1.164 -	  | rp (PDisj2(prf,tm)) thy =
   1.165 -	    let
   1.166 -		val (thy',th) = rp' prf thy
   1.167 -	    in
   1.168 -		P.DISJ2 tm th thy'
   1.169 -	    end
   1.170 -	  | rp (PDisjCases(prf,prf1,prf2)) thy =
   1.171 -	    let
   1.172 -		val (thy',th)  = rp' prf  thy
   1.173 -		val (thy1,th1) = rp' prf1 thy'
   1.174 -		val (thy2,th2) = rp' prf2 thy1
   1.175 -	    in
   1.176 -		P.DISJ_CASES th th1 th2 thy2
   1.177 -	    end
   1.178 -	  | rp (PNotI prf) thy =
   1.179 -	    let
   1.180 -		val (thy',th) = rp' prf thy
   1.181 -	    in
   1.182 -		P.NOT_INTRO th thy'
   1.183 -	    end
   1.184 -	  | rp (PNotE prf) thy =
   1.185 -	    let
   1.186 -		val (thy',th) = rp' prf thy
   1.187 -	    in
   1.188 -		P.NOT_ELIM th thy'
   1.189 -	    end
   1.190 -	  | rp (PContr(prf,tm)) thy =
   1.191 -	    let
   1.192 -		val (thy',th) = rp' prf thy
   1.193 -	    in
   1.194 -		P.CCONTR tm th thy'
   1.195 -	    end
   1.196 -	  | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   1.197 -	  | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   1.198 -	  | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
   1.199 -	  | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
   1.200 -	  | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
   1.201 -	and rp' p thy =
   1.202 -	    let
   1.203 -		val pc = content_of p
   1.204 -	    in
   1.205 -		case pc of
   1.206 -		    PDisk => (case disk_info_of p of
   1.207 -				  SOME(thyname',thmname) =>
   1.208 -				  (case Int.fromString thmname of
   1.209 -				       SOME i =>
   1.210 -				       if thyname' = thyname
   1.211 -				       then
   1.212 -					   (case Array.sub(int_thms,i-1) of
   1.213 -						NONE =>
   1.214 -						let
   1.215 -						    val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
   1.216 -						    val _ = Array.update(int_thms,i-1,SOME th)
   1.217 -						in
   1.218 -						    (thy',th)
   1.219 -						end
   1.220 -					      | SOME th => (thy,th))
   1.221 -				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   1.222 -				     | NONE => 
   1.223 -				       (case P.get_thm thyname' thmname thy of
   1.224 -					    (thy',SOME res) => (thy',res)
   1.225 -					  | (thy',NONE) => 
   1.226 -					    if thyname' = thyname
   1.227 -					    then
   1.228 -						let
   1.229 -						    val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
   1.230 -						    val (f_opt,prf) = import_proof thyname' thmname thy'
   1.231 -						    val prf = prf thy'
   1.232 -						    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
   1.233 +        val _ = ImportRecorder.start_replay_proof thyname thmname 
   1.234 +        fun rp (PRefl tm) thy = P.REFL tm thy
   1.235 +          | rp (PInstT(p,lambda)) thy =
   1.236 +            let
   1.237 +                val (thy',th) = rp' p thy
   1.238 +            in
   1.239 +                P.INST_TYPE lambda th thy'
   1.240 +            end
   1.241 +          | rp (PSubst(prfs,ctxt,prf)) thy =
   1.242 +            let
   1.243 +                val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
   1.244 +                                           let
   1.245 +                                               val (thy',th) = rp' p thy
   1.246 +                                           in
   1.247 +                                               (thy',th::ths)
   1.248 +                                           end) prfs (thy,[])
   1.249 +                val (thy'',th) = rp' prf thy'
   1.250 +            in
   1.251 +                P.SUBST ths ctxt th thy''
   1.252 +            end
   1.253 +          | rp (PAbs(prf,v)) thy =
   1.254 +            let
   1.255 +                val (thy',th) = rp' prf thy
   1.256 +            in
   1.257 +                P.ABS v th thy'
   1.258 +            end
   1.259 +          | rp (PDisch(prf,tm)) thy =
   1.260 +            let
   1.261 +                val (thy',th) = rp' prf thy
   1.262 +            in
   1.263 +                P.DISCH tm th thy'
   1.264 +            end
   1.265 +          | rp (PMp(prf1,prf2)) thy =
   1.266 +            let
   1.267 +                val (thy1,th1) = rp' prf1 thy
   1.268 +                val (thy2,th2) = rp' prf2 thy1
   1.269 +            in
   1.270 +                P.MP th1 th2 thy2
   1.271 +            end
   1.272 +          | rp (PHyp tm) thy = P.ASSUME tm thy
   1.273 +          | rp (PDef(seg,name,rhs)) thy =
   1.274 +            (case P.get_def seg name rhs thy of
   1.275 +                 (thy',SOME res) => (thy',res)
   1.276 +               | (thy',NONE) => 
   1.277 +                 if seg = thyname
   1.278 +                 then P.new_definition seg name rhs thy'
   1.279 +                 else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
   1.280 +          | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
   1.281 +          | rp (PSpec(prf,tm)) thy =
   1.282 +            let
   1.283 +                val (thy',th) = rp' prf thy
   1.284 +            in
   1.285 +                P.SPEC tm th thy'
   1.286 +            end
   1.287 +          | rp (PInst(prf,theta)) thy =
   1.288 +            let
   1.289 +                val (thy',th) = rp' prf thy
   1.290 +            in
   1.291 +                P.INST theta th thy'
   1.292 +            end
   1.293 +          | rp (PGen(prf,v)) thy =
   1.294 +            let
   1.295 +                val (thy',th) = rp' prf thy
   1.296 +                val p = P.GEN v th thy'
   1.297 +            in
   1.298 +                p
   1.299 +            end
   1.300 +          | rp (PGenAbs(prf,opt,vl)) thy =
   1.301 +            let
   1.302 +                val (thy',th) = rp' prf thy
   1.303 +            in
   1.304 +                P.GEN_ABS opt vl th thy'
   1.305 +            end
   1.306 +          | rp (PImpAS(prf1,prf2)) thy =
   1.307 +            let
   1.308 +                val (thy1,th1) = rp' prf1 thy
   1.309 +                val (thy2,th2) = rp' prf2 thy1
   1.310 +            in
   1.311 +                P.IMP_ANTISYM th1 th2 thy2
   1.312 +            end
   1.313 +          | rp (PSym prf) thy =
   1.314 +            let
   1.315 +                val (thy1,th) = rp' prf thy
   1.316 +            in
   1.317 +                P.SYM th thy1
   1.318 +            end
   1.319 +          | rp (PTrans(prf1,prf2)) thy =
   1.320 +            let
   1.321 +                val (thy1,th1) = rp' prf1 thy
   1.322 +                val (thy2,th2) = rp' prf2 thy1
   1.323 +            in
   1.324 +                P.TRANS th1 th2 thy2
   1.325 +            end
   1.326 +          | rp (PComb(prf1,prf2)) thy =
   1.327 +            let
   1.328 +                val (thy1,th1) = rp' prf1 thy
   1.329 +                val (thy2,th2) = rp' prf2 thy1
   1.330 +            in
   1.331 +                P.COMB th1 th2 thy2
   1.332 +            end
   1.333 +          | rp (PEqMp(prf1,prf2)) thy =
   1.334 +            let
   1.335 +                val (thy1,th1) = rp' prf1 thy
   1.336 +                val (thy2,th2) = rp' prf2 thy1
   1.337 +            in
   1.338 +                P.EQ_MP th1 th2 thy2
   1.339 +            end
   1.340 +          | rp (PEqImp prf) thy =
   1.341 +            let
   1.342 +                val (thy',th) = rp' prf thy
   1.343 +            in
   1.344 +                P.EQ_IMP_RULE th thy'
   1.345 +            end
   1.346 +          | rp (PExists(prf,ex,wit)) thy =
   1.347 +            let
   1.348 +                val (thy',th) = rp' prf thy
   1.349 +            in
   1.350 +                P.EXISTS ex wit th thy'
   1.351 +            end
   1.352 +          | rp (PChoose(v,prf1,prf2)) thy =
   1.353 +            let
   1.354 +                val (thy1,th1) = rp' prf1 thy
   1.355 +                val (thy2,th2) = rp' prf2 thy1
   1.356 +            in
   1.357 +                P.CHOOSE v th1 th2 thy2
   1.358 +            end
   1.359 +          | rp (PConj(prf1,prf2)) thy =
   1.360 +            let
   1.361 +                val (thy1,th1) = rp' prf1 thy
   1.362 +                val (thy2,th2) = rp' prf2 thy1
   1.363 +            in
   1.364 +                P.CONJ th1 th2 thy2
   1.365 +            end
   1.366 +          | rp (PConjunct1 prf) thy =
   1.367 +            let
   1.368 +                val (thy',th) = rp' prf thy
   1.369 +            in
   1.370 +                P.CONJUNCT1 th thy'
   1.371 +            end
   1.372 +          | rp (PConjunct2 prf) thy =
   1.373 +            let
   1.374 +                val (thy',th) = rp' prf thy
   1.375 +            in
   1.376 +                P.CONJUNCT2 th thy'
   1.377 +            end
   1.378 +          | rp (PDisj1(prf,tm)) thy =
   1.379 +            let
   1.380 +                val (thy',th) = rp' prf thy
   1.381 +            in
   1.382 +                P.DISJ1 th tm thy'
   1.383 +            end
   1.384 +          | rp (PDisj2(prf,tm)) thy =
   1.385 +            let
   1.386 +                val (thy',th) = rp' prf thy
   1.387 +            in
   1.388 +                P.DISJ2 tm th thy'
   1.389 +            end
   1.390 +          | rp (PDisjCases(prf,prf1,prf2)) thy =
   1.391 +            let
   1.392 +                val (thy',th)  = rp' prf  thy
   1.393 +                val (thy1,th1) = rp' prf1 thy'
   1.394 +                val (thy2,th2) = rp' prf2 thy1
   1.395 +            in
   1.396 +                P.DISJ_CASES th th1 th2 thy2
   1.397 +            end
   1.398 +          | rp (PNotI prf) thy =
   1.399 +            let
   1.400 +                val (thy',th) = rp' prf thy
   1.401 +            in
   1.402 +                P.NOT_INTRO th thy'
   1.403 +            end
   1.404 +          | rp (PNotE prf) thy =
   1.405 +            let
   1.406 +                val (thy',th) = rp' prf thy
   1.407 +            in
   1.408 +                P.NOT_ELIM th thy'
   1.409 +            end
   1.410 +          | rp (PContr(prf,tm)) thy =
   1.411 +            let
   1.412 +                val (thy',th) = rp' prf thy
   1.413 +            in
   1.414 +                P.CCONTR tm th thy'
   1.415 +            end
   1.416 +          | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
   1.417 +          | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
   1.418 +          | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
   1.419 +          | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
   1.420 +          | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
   1.421 +        and rp' p thy =
   1.422 +            let
   1.423 +                val pc = content_of p
   1.424 +            in
   1.425 +                case pc of
   1.426 +                    PDisk => (case disk_info_of p of
   1.427 +                                  SOME(thyname',thmname) =>
   1.428 +                                  (case Int.fromString thmname of
   1.429 +                                       SOME i =>
   1.430 +                                       if thyname' = thyname
   1.431 +                                       then
   1.432 +                                           (case Array.sub(int_thms,i-1) of
   1.433 +                                                NONE =>
   1.434 +                                                let
   1.435 +                                                    val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
   1.436 +                                                    val _ = Array.update(int_thms,i-1,SOME th)
   1.437 +                                                in
   1.438 +                                                    (thy',th)
   1.439 +                                                end
   1.440 +                                              | SOME th => (thy,th))
   1.441 +                                       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
   1.442 +                                     | NONE => 
   1.443 +                                       (case P.get_thm thyname' thmname thy of
   1.444 +                                            (thy',SOME res) => (thy',res)
   1.445 +                                          | (thy',NONE) => 
   1.446 +                                            if thyname' = thyname
   1.447 +                                            then
   1.448 +                                                let
   1.449 +                                                    val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
   1.450 +                                                    val (f_opt,prf) = import_proof thyname' thmname thy'
   1.451 +                                                    val prf = prf thy'
   1.452 +                                                    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
   1.453                                                      val _ = writeln ("Successfully finished replaying "^thmname^" !")
   1.454 -						in
   1.455 -						    case content_of prf of
   1.456 -							PTmSpec _ => (thy',th)
   1.457 -						      | PTyDef  _ => (thy',th)
   1.458 -						      | PTyIntro _ => (thy',th)
   1.459 -						      | _ => P.store_thm thyname' thmname th thy'
   1.460 -						end
   1.461 -					    else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   1.462 -				| NONE => raise ERR "rp'.PDisk" "Not enough information")
   1.463 -		  | PAxm(name,c) =>
   1.464 -		    (case P.get_axiom thyname name thy of
   1.465 -			    (thy',SOME res) => (thy',res)
   1.466 -			  | (thy',NONE) => P.new_axiom name c thy')
   1.467 -		  | PTmSpec(seg,names,prf') =>
   1.468 -		    let
   1.469 -			val (thy',th) = rp' prf' thy
   1.470 -		    in
   1.471 -			P.new_specification seg thmname names th thy'
   1.472 -		    end
   1.473 -		  | PTyDef(seg,name,prf') =>
   1.474 -		    let
   1.475 -			val (thy',th) = rp' prf' thy
   1.476 -		    in
   1.477 -			P.new_type_definition seg thmname name th thy'
   1.478 -		    end
   1.479 -		  | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   1.480 -		    let
   1.481 -			val (thy',th) = rp' prf' thy
   1.482 -		    in
   1.483 -			P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   1.484 -		    end
   1.485 -		  | _ => rp pc thy
   1.486 -	    end
   1.487 +                                                in
   1.488 +                                                    case content_of prf of
   1.489 +                                                        PTmSpec _ => (thy',th)
   1.490 +                                                      | PTyDef  _ => (thy',th)
   1.491 +                                                      | PTyIntro _ => (thy',th)
   1.492 +                                                      | _ => P.store_thm thyname' thmname th thy'
   1.493 +                                                end
   1.494 +                                            else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
   1.495 +                                | NONE => raise ERR "rp'.PDisk" "Not enough information")
   1.496 +                  | PAxm(name,c) =>
   1.497 +                    (case P.get_axiom thyname name thy of
   1.498 +                            (thy',SOME res) => (thy',res)
   1.499 +                          | (thy',NONE) => P.new_axiom name c thy')
   1.500 +                  | PTmSpec(seg,names,prf') =>
   1.501 +                    let
   1.502 +                        val (thy',th) = rp' prf' thy
   1.503 +                    in
   1.504 +                        P.new_specification seg thmname names th thy'
   1.505 +                    end
   1.506 +                  | PTyDef(seg,name,prf') =>
   1.507 +                    let
   1.508 +                        val (thy',th) = rp' prf' thy
   1.509 +                    in
   1.510 +                        P.new_type_definition seg thmname name th thy'
   1.511 +                    end
   1.512 +                  | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
   1.513 +                    let
   1.514 +                        val (thy',th) = rp' prf' thy
   1.515 +                    in
   1.516 +                        P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
   1.517 +                    end
   1.518 +                  | _ => rp pc thy
   1.519 +            end
   1.520      in
   1.521 -	let
   1.522 -	    val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
   1.523 -	    val _ = ImportRecorder.stop_replay_proof thyname thmname
   1.524 -	in
   1.525 -	    x
   1.526 -	end
   1.527 +        let
   1.528 +            val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
   1.529 +            val _ = ImportRecorder.stop_replay_proof thyname thmname
   1.530 +        in
   1.531 +            x
   1.532 +        end
   1.533      end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
   1.534  
   1.535  fun setup_int_thms thyname thy =
   1.536      let
   1.537 -	val fname =
   1.538 -	    case P.get_proof_dir thyname thy of
   1.539 -		SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   1.540 -	      | NONE => error "Cannot find proof files"
   1.541 -	val is = TextIO.openIn fname
   1.542 -	val (num_int_thms,facts) =
   1.543 -	    let
   1.544 -		fun get_facts facts =
   1.545 -		    case TextIO.inputLine is of
   1.546 -			NONE => (case facts of
   1.547 -				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
   1.548 -				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
   1.549 -		      | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   1.550 -	    in
   1.551 -		get_facts []
   1.552 -	    end
   1.553 -	val _ = TextIO.closeIn is
   1.554 -	val int_thms = Array.array(num_int_thms,NONE:thm option)
   1.555 +        val fname =
   1.556 +            case P.get_proof_dir thyname thy of
   1.557 +                SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   1.558 +              | NONE => error "Cannot find proof files"
   1.559 +        val is = TextIO.openIn fname
   1.560 +        val (num_int_thms,facts) =
   1.561 +            let
   1.562 +                fun get_facts facts =
   1.563 +                    case TextIO.inputLine is of
   1.564 +                        NONE => (case facts of
   1.565 +                                   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
   1.566 +                                 | _ => raise ERR "replay_thm" "Bad facts.lst file")
   1.567 +                      | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
   1.568 +            in
   1.569 +                get_facts []
   1.570 +            end
   1.571 +        val _ = TextIO.closeIn is
   1.572 +        val int_thms = Array.array(num_int_thms,NONE:thm option)
   1.573      in
   1.574 -	(int_thms,facts)
   1.575 +        (int_thms,facts)
   1.576      end
   1.577  
   1.578  fun import_single_thm thyname int_thms thmname thy =
   1.579      let
   1.580 -	fun replay_fact (thmname,thy) =
   1.581 -	    let
   1.582 -		val prf = mk_proof PDisk
   1.583 -		val _ = set_disk_info_of prf thyname thmname
   1.584 +        fun replay_fact (thmname,thy) =
   1.585 +            let
   1.586 +                val prf = mk_proof PDisk
   1.587 +                val _ = set_disk_info_of prf thyname thmname
   1.588                  val _ = writeln ("Replaying "^thmname^" ...")
   1.589 -		val p = fst (replay_proof int_thms thyname thmname prf thy)
   1.590 -	    in
   1.591 -		p
   1.592 -	    end
   1.593 +                val p = fst (replay_proof int_thms thyname thmname prf thy)
   1.594 +            in
   1.595 +                p
   1.596 +            end
   1.597      in
   1.598 -	replay_fact (thmname,thy)
   1.599 +        replay_fact (thmname,thy)
   1.600      end
   1.601  
   1.602  fun replay_chached_thm int_thms thyname thmname =
   1.603      let
   1.604 -	fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
   1.605 -	fun err msg = raise ERR "replay_cached_thm" msg
   1.606 -	val _ = writeln ("Replaying (from cache) "^thmname^" ...")
   1.607 -	fun rps [] thy = thy
   1.608 -	  | rps (t::ts) thy = rps ts (rp t thy)
   1.609 -	and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy	    
   1.610 -	  | rp (DeltaEntry ds) thy = fold delta ds thy
   1.611 -	and delta (Specification (names, th)) thy = 
   1.612 -	    fst (Choice_Specification.add_specification NONE names (thy,th_of thy th))
   1.613 -	  | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
   1.614 -	    add_hol4_mapping thyname thmname isaname thy
   1.615 -	  | delta (Hol_pending (thyname, thmname, th)) thy = 
   1.616 -	    add_hol4_pending thyname thmname ([], th_of thy th) thy
   1.617 -	  | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
   1.618 -	  | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
   1.619 -	    add_hol4_const_mapping thyname constname true fullcname thy
   1.620 -	  | delta (Hol_move (fullname, moved_thmname)) thy = 
   1.621 -	    add_hol4_move fullname moved_thmname thy
   1.622 -	  | delta (Defs (thmname, eq)) thy =
   1.623 -	    snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
   1.624 -	  | delta (Hol_theorem (thyname, thmname, th)) thy =
   1.625 -	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
   1.626 -	  | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
   1.627 -	    snd (Typedef.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
   1.628 +        fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
   1.629 +        fun err msg = raise ERR "replay_cached_thm" msg
   1.630 +        val _ = writeln ("Replaying (from cache) "^thmname^" ...")
   1.631 +        fun rps [] thy = thy
   1.632 +          | rps (t::ts) thy = rps ts (rp t thy)
   1.633 +        and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy      
   1.634 +          | rp (DeltaEntry ds) thy = fold delta ds thy
   1.635 +        and delta (Specification (names, th)) thy = 
   1.636 +            fst (Choice_Specification.add_specification NONE names (thy,th_of thy th))
   1.637 +          | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
   1.638 +            add_hol4_mapping thyname thmname isaname thy
   1.639 +          | delta (Hol_pending (thyname, thmname, th)) thy = 
   1.640 +            add_hol4_pending thyname thmname ([], th_of thy th) thy
   1.641 +          | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
   1.642 +          | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
   1.643 +            add_hol4_const_mapping thyname constname true fullcname thy
   1.644 +          | delta (Hol_move (fullname, moved_thmname)) thy = 
   1.645 +            add_hol4_move fullname moved_thmname thy
   1.646 +          | delta (Defs (thmname, eq)) thy =
   1.647 +            snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
   1.648 +          | delta (Hol_theorem (thyname, thmname, th)) thy =
   1.649 +            add_hol4_theorem thyname thmname ([], th_of thy th) thy
   1.650 +          | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
   1.651 +            snd (Typedef.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
   1.652          (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
   1.653 -	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
   1.654 -	    add_hol4_type_mapping thyname tycname true fulltyname thy
   1.655 -	  | delta (Indexed_theorem (i, th)) thy = 
   1.656 -	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
   1.657 +          | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
   1.658 +            add_hol4_type_mapping thyname tycname true fulltyname thy
   1.659 +          | delta (Indexed_theorem (i, th)) thy = 
   1.660 +            (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)                   
   1.661            | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
   1.662 -	  | delta (Dump s) thy = P.replay_add_dump s thy
   1.663 +          | delta (Dump s) thy = P.replay_add_dump s thy
   1.664      in
   1.665 -	rps
   1.666 +        rps
   1.667      end
   1.668  
   1.669  fun import_thms thyname int_thms thmnames thy =
   1.670      let
   1.671 -	fun zip names [] = ([], names)
   1.672 -	  | zip [] _ = ([], [])
   1.673 -	  | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 
   1.674 -	    if thyname = thyname' andalso thmname = thmname' then
   1.675 -		(if aborted then ([], thmname::names) else 
   1.676 -		 let
   1.677 -		     val _ = writeln ("theorem is in-sync: "^thmname)
   1.678 -		     val (cached,normal) = zip names ys
   1.679 -		 in
   1.680 -		     (entry::cached, normal)
   1.681 -		 end)
   1.682 -	    else
   1.683 -		let
   1.684 -		    val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
   1.685 -		    val _ = writeln ("proceeding with next uncached theorem...")
   1.686 -		in
   1.687 -		    ([], thmname::names)
   1.688 -		end
   1.689 -	(*	raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
   1.690 -	  | zip (thmname::_) (DeltaEntry _ :: _) = 
   1.691 - 	    raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
   1.692 -	fun zip' xs (History ys) = 
   1.693 -	    let
   1.694 -		val _ = writeln ("length of xs: "^(string_of_int (length xs)))
   1.695 -		val _ = writeln ("length of history: "^(string_of_int (length ys)))
   1.696 -	    in
   1.697 -		zip xs ys
   1.698 -	    end
   1.699 -	fun replay_fact thmname thy = 
   1.700 -	    let
   1.701 -		val prf = mk_proof PDisk	
   1.702 -		val _ = set_disk_info_of prf thyname thmname
   1.703 +        fun zip names [] = ([], names)
   1.704 +          | zip [] _ = ([], [])
   1.705 +          | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 
   1.706 +            if thyname = thyname' andalso thmname = thmname' then
   1.707 +                (if aborted then ([], thmname::names) else 
   1.708 +                 let
   1.709 +                     val _ = writeln ("theorem is in-sync: "^thmname)
   1.710 +                     val (cached,normal) = zip names ys
   1.711 +                 in
   1.712 +                     (entry::cached, normal)
   1.713 +                 end)
   1.714 +            else
   1.715 +                let
   1.716 +                    val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
   1.717 +                    val _ = writeln ("proceeding with next uncached theorem...")
   1.718 +                in
   1.719 +                    ([], thmname::names)
   1.720 +                end
   1.721 +        (*      raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
   1.722 +          | zip (thmname::_) (DeltaEntry _ :: _) = 
   1.723 +            raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
   1.724 +        fun zip' xs (History ys) = 
   1.725 +            let
   1.726 +                val _ = writeln ("length of xs: "^(string_of_int (length xs)))
   1.727 +                val _ = writeln ("length of history: "^(string_of_int (length ys)))
   1.728 +            in
   1.729 +                zip xs ys
   1.730 +            end
   1.731 +        fun replay_fact thmname thy = 
   1.732 +            let
   1.733 +                val prf = mk_proof PDisk        
   1.734 +                val _ = set_disk_info_of prf thyname thmname
   1.735                  val _ = writeln ("Replaying "^thmname^" ...")
   1.736 -		val p = fst (replay_proof int_thms thyname thmname prf thy)
   1.737 -	    in
   1.738 -		p
   1.739 -	    end
   1.740 -	fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
   1.741 -	val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
   1.742 -	val _ = ImportRecorder.set_history (History (map ThmEntry cached))
   1.743 -	val res_thy = fold replay_fact normal (fold replay_cache cached thy)
   1.744 +                val p = fst (replay_proof int_thms thyname thmname prf thy)
   1.745 +            in
   1.746 +                p
   1.747 +            end
   1.748 +        fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
   1.749 +        val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
   1.750 +        val _ = ImportRecorder.set_history (History (map ThmEntry cached))
   1.751 +        val res_thy = fold replay_fact normal (fold replay_cache cached thy)
   1.752      in
   1.753 -	res_thy
   1.754 +        res_thy
   1.755      end
   1.756  
   1.757  fun import_thm thyname thmname thy =
   1.758      let
   1.759 -	val int_thms = fst (setup_int_thms thyname thy)
   1.760 -	fun replay_fact (thmname,thy) =
   1.761 -	    let
   1.762 -		val prf = mk_proof PDisk	
   1.763 -		val _ = set_disk_info_of prf thyname thmname 	    
   1.764 +        val int_thms = fst (setup_int_thms thyname thy)
   1.765 +        fun replay_fact (thmname,thy) =
   1.766 +            let
   1.767 +                val prf = mk_proof PDisk        
   1.768 +                val _ = set_disk_info_of prf thyname thmname        
   1.769                  val _ = writeln ("Replaying "^thmname^" ...")
   1.770 -		val p = fst (replay_proof int_thms thyname thmname prf thy)
   1.771 -	    in 
   1.772 -		p
   1.773 -	    end
   1.774 +                val p = fst (replay_proof int_thms thyname thmname prf thy)
   1.775 +            in 
   1.776 +                p
   1.777 +            end
   1.778      in
   1.779 -	replay_fact (thmname,thy)
   1.780 +        replay_fact (thmname,thy)
   1.781      end
   1.782  
   1.783  end