src/HOL/Import/replay.ML
author haftmann
Wed Jan 21 18:27:43 2009 +0100 (2009-01-21)
changeset 29585 c23295521af5
parent 28662 64ab5bb68d4c
child 30346 90efbb8a8cb2
permissions -rw-r--r--
binding replaces bstring
skalberg@14620
     1
(*  Title:      HOL/Import/replay.ML
skalberg@14620
     2
    ID:         $Id$
skalberg@14620
     3
    Author:     Sebastian Skalberg (TU Muenchen)
skalberg@14620
     4
*)
skalberg@14620
     5
skalberg@14516
     6
structure Replay =
skalberg@14516
     7
struct
skalberg@14516
     8
skalberg@14516
     9
structure P = ProofKernel
skalberg@14516
    10
skalberg@14516
    11
open ProofKernel
obua@19064
    12
open ImportRecorder
skalberg@14516
    13
skalberg@14516
    14
exception REPLAY of string * string
skalberg@14516
    15
fun ERR f mesg = REPLAY (f,mesg)
skalberg@14516
    16
fun NY f = raise ERR f "NOT YET!"
skalberg@14516
    17
skalberg@14516
    18
fun replay_proof int_thms thyname thmname prf thy =
skalberg@14516
    19
    let
obua@19064
    20
	val _ = ImportRecorder.start_replay_proof thyname thmname 
skalberg@14516
    21
	fun rp (PRefl tm) thy = P.REFL tm thy
skalberg@14516
    22
	  | rp (PInstT(p,lambda)) thy =
skalberg@14516
    23
	    let
skalberg@14516
    24
		val (thy',th) = rp' p thy
skalberg@14516
    25
	    in
skalberg@14516
    26
		P.INST_TYPE lambda th thy'
skalberg@14516
    27
	    end
skalberg@14516
    28
	  | rp (PSubst(prfs,ctxt,prf)) thy =
skalberg@14516
    29
	    let
haftmann@21078
    30
		val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
skalberg@14516
    31
					   let
skalberg@14516
    32
					       val (thy',th) = rp' p thy
skalberg@14516
    33
					   in
skalberg@14516
    34
					       (thy',th::ths)
haftmann@21078
    35
					   end) prfs (thy,[])
skalberg@14516
    36
		val (thy'',th) = rp' prf thy'
skalberg@14516
    37
	    in
skalberg@14516
    38
		P.SUBST ths ctxt th thy''
skalberg@14516
    39
	    end
skalberg@14516
    40
	  | rp (PAbs(prf,v)) thy =
skalberg@14516
    41
	    let
skalberg@14516
    42
		val (thy',th) = rp' prf thy
skalberg@14516
    43
	    in
skalberg@14516
    44
		P.ABS v th thy'
skalberg@14516
    45
	    end
skalberg@14516
    46
	  | rp (PDisch(prf,tm)) thy =
skalberg@14516
    47
	    let
skalberg@14516
    48
		val (thy',th) = rp' prf thy
skalberg@14516
    49
	    in
skalberg@14516
    50
		P.DISCH tm th thy'
skalberg@14516
    51
	    end
skalberg@14516
    52
	  | rp (PMp(prf1,prf2)) thy =
skalberg@14516
    53
	    let
skalberg@14516
    54
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
    55
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
    56
	    in
skalberg@14516
    57
		P.MP th1 th2 thy2
skalberg@14516
    58
	    end
skalberg@14516
    59
	  | rp (PHyp tm) thy = P.ASSUME tm thy
skalberg@14516
    60
	  | rp (PDef(seg,name,rhs)) thy =
skalberg@14516
    61
	    (case P.get_def seg name rhs thy of
skalberg@15531
    62
		 (thy',SOME res) => (thy',res)
skalberg@15531
    63
	       | (thy',NONE) => 
skalberg@14516
    64
		 if seg = thyname
skalberg@14516
    65
		 then P.new_definition seg name rhs thy'
obua@17322
    66
		 else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
skalberg@14516
    67
	  | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
skalberg@14516
    68
	  | rp (PSpec(prf,tm)) thy =
skalberg@14516
    69
	    let
skalberg@14516
    70
		val (thy',th) = rp' prf thy
skalberg@14516
    71
	    in
skalberg@14516
    72
		P.SPEC tm th thy'
skalberg@14516
    73
	    end
skalberg@14516
    74
	  | rp (PInst(prf,theta)) thy =
skalberg@14516
    75
	    let
skalberg@14516
    76
		val (thy',th) = rp' prf thy
skalberg@14516
    77
	    in
skalberg@14516
    78
		P.INST theta th thy'
skalberg@14516
    79
	    end
skalberg@14516
    80
	  | rp (PGen(prf,v)) thy =
skalberg@14516
    81
	    let
skalberg@14516
    82
		val (thy',th) = rp' prf thy
obua@17592
    83
		val p = P.GEN v th thy'
skalberg@14516
    84
	    in
obua@17592
    85
		p
skalberg@14516
    86
	    end
skalberg@14516
    87
	  | rp (PGenAbs(prf,opt,vl)) thy =
skalberg@14516
    88
	    let
skalberg@14516
    89
		val (thy',th) = rp' prf thy
skalberg@14516
    90
	    in
skalberg@14516
    91
		P.GEN_ABS opt vl th thy'
skalberg@14516
    92
	    end
skalberg@14516
    93
	  | rp (PImpAS(prf1,prf2)) thy =
skalberg@14516
    94
	    let
skalberg@14516
    95
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
    96
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
    97
	    in
skalberg@14516
    98
		P.IMP_ANTISYM th1 th2 thy2
skalberg@14516
    99
	    end
skalberg@14516
   100
	  | rp (PSym prf) thy =
skalberg@14516
   101
	    let
skalberg@14516
   102
		val (thy1,th) = rp' prf thy
skalberg@14516
   103
	    in
skalberg@14516
   104
		P.SYM th thy1
skalberg@14516
   105
	    end
skalberg@14516
   106
	  | rp (PTrans(prf1,prf2)) thy =
skalberg@14516
   107
	    let
skalberg@14516
   108
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   109
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   110
	    in
skalberg@14516
   111
		P.TRANS th1 th2 thy2
skalberg@14516
   112
	    end
skalberg@14516
   113
	  | rp (PComb(prf1,prf2)) thy =
skalberg@14516
   114
	    let
skalberg@14516
   115
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   116
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   117
	    in
skalberg@14516
   118
		P.COMB th1 th2 thy2
skalberg@14516
   119
	    end
skalberg@14516
   120
	  | rp (PEqMp(prf1,prf2)) thy =
skalberg@14516
   121
	    let
skalberg@14516
   122
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   123
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   124
	    in
skalberg@14516
   125
		P.EQ_MP th1 th2 thy2
skalberg@14516
   126
	    end
skalberg@14516
   127
	  | rp (PEqImp prf) thy =
skalberg@14516
   128
	    let
skalberg@14516
   129
		val (thy',th) = rp' prf thy
skalberg@14516
   130
	    in
skalberg@14516
   131
		P.EQ_IMP_RULE th thy'
skalberg@14516
   132
	    end
skalberg@14516
   133
	  | rp (PExists(prf,ex,wit)) thy =
skalberg@14516
   134
	    let
skalberg@14516
   135
		val (thy',th) = rp' prf thy
skalberg@14516
   136
	    in
skalberg@14516
   137
		P.EXISTS ex wit th thy'
skalberg@14516
   138
	    end
skalberg@14516
   139
	  | rp (PChoose(v,prf1,prf2)) thy =
skalberg@14516
   140
	    let
skalberg@14516
   141
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   142
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   143
	    in
skalberg@14516
   144
		P.CHOOSE v th1 th2 thy2
skalberg@14516
   145
	    end
skalberg@14516
   146
	  | rp (PConj(prf1,prf2)) thy =
skalberg@14516
   147
	    let
skalberg@14516
   148
		val (thy1,th1) = rp' prf1 thy
skalberg@14516
   149
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   150
	    in
skalberg@14516
   151
		P.CONJ th1 th2 thy2
skalberg@14516
   152
	    end
skalberg@14516
   153
	  | rp (PConjunct1 prf) thy =
skalberg@14516
   154
	    let
skalberg@14516
   155
		val (thy',th) = rp' prf thy
skalberg@14516
   156
	    in
skalberg@14516
   157
		P.CONJUNCT1 th thy'
skalberg@14516
   158
	    end
skalberg@14516
   159
	  | rp (PConjunct2 prf) thy =
skalberg@14516
   160
	    let
skalberg@14516
   161
		val (thy',th) = rp' prf thy
skalberg@14516
   162
	    in
skalberg@14516
   163
		P.CONJUNCT2 th thy'
skalberg@14516
   164
	    end
skalberg@14516
   165
	  | rp (PDisj1(prf,tm)) thy =
skalberg@14516
   166
	    let
skalberg@14516
   167
		val (thy',th) = rp' prf thy
skalberg@14516
   168
	    in
skalberg@14516
   169
		P.DISJ1 th tm thy'
skalberg@14516
   170
	    end
skalberg@14516
   171
	  | rp (PDisj2(prf,tm)) thy =
skalberg@14516
   172
	    let
skalberg@14516
   173
		val (thy',th) = rp' prf thy
skalberg@14516
   174
	    in
skalberg@14516
   175
		P.DISJ2 tm th thy'
skalberg@14516
   176
	    end
skalberg@14516
   177
	  | rp (PDisjCases(prf,prf1,prf2)) thy =
skalberg@14516
   178
	    let
skalberg@14516
   179
		val (thy',th)  = rp' prf  thy
skalberg@14516
   180
		val (thy1,th1) = rp' prf1 thy'
skalberg@14516
   181
		val (thy2,th2) = rp' prf2 thy1
skalberg@14516
   182
	    in
skalberg@14516
   183
		P.DISJ_CASES th th1 th2 thy2
skalberg@14516
   184
	    end
skalberg@14516
   185
	  | rp (PNotI prf) thy =
skalberg@14516
   186
	    let
skalberg@14516
   187
		val (thy',th) = rp' prf thy
skalberg@14516
   188
	    in
skalberg@14516
   189
		P.NOT_INTRO th thy'
skalberg@14516
   190
	    end
skalberg@14516
   191
	  | rp (PNotE prf) thy =
skalberg@14516
   192
	    let
skalberg@14516
   193
		val (thy',th) = rp' prf thy
skalberg@14516
   194
	    in
skalberg@14516
   195
		P.NOT_ELIM th thy'
skalberg@14516
   196
	    end
skalberg@14516
   197
	  | rp (PContr(prf,tm)) thy =
skalberg@14516
   198
	    let
skalberg@14516
   199
		val (thy',th) = rp' prf thy
skalberg@14516
   200
	    in
skalberg@14516
   201
		P.CCONTR tm th thy'
skalberg@14516
   202
	    end
skalberg@14516
   203
	  | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
skalberg@14516
   204
	  | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
skalberg@14516
   205
	  | rp (PTyIntro _) _ = raise ERR "rp" "Shouldn't reach here (PTyIntro)"
skalberg@14516
   206
	  | rp PDisk _ = raise ERR "rp" "Shouldn't reach here (PDisk)"
skalberg@14516
   207
	  | rp _ _ = raise ERR "rp" "What the hell is this? Which case did I forget?"
skalberg@14516
   208
	and rp' p thy =
skalberg@14516
   209
	    let
skalberg@14516
   210
		val pc = content_of p
skalberg@14516
   211
	    in
skalberg@14516
   212
		case pc of
skalberg@14516
   213
		    PDisk => (case disk_info_of p of
skalberg@15531
   214
				  SOME(thyname',thmname) =>
skalberg@14516
   215
				  (case Int.fromString thmname of
skalberg@14516
   216
				       SOME i =>
skalberg@14516
   217
				       if thyname' = thyname
skalberg@14516
   218
				       then
skalberg@14516
   219
					   (case Array.sub(int_thms,i-1) of
skalberg@15531
   220
						NONE =>
skalberg@14516
   221
						let
skalberg@14516
   222
						    val (thy',th) = rp' (snd (import_proof thyname' thmname thy) thy) thy
skalberg@15531
   223
						    val _ = Array.update(int_thms,i-1,SOME th)
skalberg@14516
   224
						in
skalberg@14516
   225
						    (thy',th)
skalberg@14516
   226
						end
skalberg@15531
   227
					      | SOME th => (thy,th))
skalberg@14516
   228
				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
skalberg@14516
   229
				     | NONE => 
skalberg@14516
   230
				       (case P.get_thm thyname' thmname thy of
obua@17594
   231
					    (thy',SOME res) => (thy',res)
skalberg@15531
   232
					  | (thy',NONE) => 
skalberg@14516
   233
					    if thyname' = thyname
skalberg@14516
   234
					    then
skalberg@14516
   235
						let
skalberg@14516
   236
						    val _ = writeln ("Found no " ^ thmname ^ " theorem, replaying...")
skalberg@14516
   237
						    val (f_opt,prf) = import_proof thyname' thmname thy'
skalberg@14516
   238
						    val prf = prf thy'
skalberg@14516
   239
						    val (thy',th) = replay_proof int_thms thyname' thmname prf thy'
obua@17322
   240
                                                    val _ = writeln ("Successfully finished replaying "^thmname^" !")
skalberg@14516
   241
						in
skalberg@14516
   242
						    case content_of prf of
skalberg@14516
   243
							PTmSpec _ => (thy',th)
skalberg@14516
   244
						      | PTyDef  _ => (thy',th)
skalberg@14516
   245
						      | PTyIntro _ => (thy',th)
skalberg@14516
   246
						      | _ => P.store_thm thyname' thmname th thy'
skalberg@14516
   247
						end
skalberg@14516
   248
					    else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
skalberg@15531
   249
				| NONE => raise ERR "rp'.PDisk" "Not enough information")
skalberg@14516
   250
		  | PAxm(name,c) =>
skalberg@14516
   251
		    (case P.get_axiom thyname name thy of
skalberg@15531
   252
			    (thy',SOME res) => (thy',res)
skalberg@15531
   253
			  | (thy',NONE) => P.new_axiom name c thy')
skalberg@14516
   254
		  | PTmSpec(seg,names,prf') =>
skalberg@14516
   255
		    let
skalberg@14516
   256
			val (thy',th) = rp' prf' thy
skalberg@14516
   257
		    in
skalberg@14516
   258
			P.new_specification seg thmname names th thy'
skalberg@14516
   259
		    end
skalberg@14516
   260
		  | PTyDef(seg,name,prf') =>
skalberg@14516
   261
		    let
skalberg@14516
   262
			val (thy',th) = rp' prf' thy
skalberg@14516
   263
		    in
skalberg@14516
   264
			P.new_type_definition seg thmname name th thy'
skalberg@14516
   265
		    end
skalberg@14516
   266
		  | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
skalberg@14516
   267
		    let
skalberg@14516
   268
			val (thy',th) = rp' prf' thy
skalberg@14516
   269
		    in
skalberg@14516
   270
			P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
skalberg@14516
   271
		    end
skalberg@14516
   272
		  | _ => rp pc thy
skalberg@14516
   273
	    end
skalberg@14516
   274
    in
obua@19064
   275
	let
obua@19064
   276
	    val x = rp' prf thy handle e => (writeln "Exception in replay_proof"; OldGoals.print_exn e)
obua@19064
   277
	    val _ = ImportRecorder.stop_replay_proof thyname thmname
obua@19064
   278
	in
obua@19064
   279
	    x
obua@19064
   280
	end
obua@19064
   281
    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; raise x)
skalberg@14516
   282
skalberg@14516
   283
fun setup_int_thms thyname thy =
skalberg@14516
   284
    let
skalberg@14620
   285
	val fname =
skalberg@14620
   286
	    case P.get_proof_dir thyname thy of
skalberg@15531
   287
		SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
skalberg@15531
   288
	      | NONE => error "Cannot find proof files"
skalberg@14620
   289
	val is = TextIO.openIn fname
skalberg@14516
   290
	val (num_int_thms,facts) =
skalberg@14516
   291
	    let
skalberg@14516
   292
		fun get_facts facts =
skalberg@14516
   293
		    case TextIO.inputLine is of
wenzelm@23139
   294
			NONE => (case facts of
obua@17440
   295
				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
skalberg@14516
   296
				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
wenzelm@23139
   297
		      | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
skalberg@14516
   298
	    in
skalberg@14516
   299
		get_facts []
skalberg@14516
   300
	    end
skalberg@14516
   301
	val _ = TextIO.closeIn is
skalberg@15531
   302
	val int_thms = Array.array(num_int_thms,NONE:thm option)
skalberg@14516
   303
    in
skalberg@14516
   304
	(int_thms,facts)
skalberg@14516
   305
    end
skalberg@14516
   306
skalberg@14516
   307
fun import_single_thm thyname int_thms thmname thy =
skalberg@14516
   308
    let
skalberg@14516
   309
	fun replay_fact (thmname,thy) =
skalberg@14516
   310
	    let
skalberg@14516
   311
		val prf = mk_proof PDisk
skalberg@14516
   312
		val _ = set_disk_info_of prf thyname thmname
obua@17594
   313
                val _ = writeln ("Replaying "^thmname^" ...")
obua@17592
   314
		val p = fst (replay_proof int_thms thyname thmname prf thy)
skalberg@14516
   315
	    in
obua@17592
   316
		p
skalberg@14516
   317
	    end
skalberg@14516
   318
    in
skalberg@14516
   319
	replay_fact (thmname,thy)
skalberg@14516
   320
    end
skalberg@14516
   321
obua@19064
   322
fun replay_chached_thm int_thms thyname thmname =
obua@19064
   323
    let
obua@19064
   324
	fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
obua@19064
   325
	fun err msg = raise ERR "replay_cached_thm" msg
obua@19064
   326
	val _ = writeln ("Replaying (from cache) "^thmname^" ...")
obua@19064
   327
	fun rps [] thy = thy
obua@19064
   328
	  | rps (t::ts) thy = rps ts (rp t thy)
obua@19064
   329
	and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy	    
obua@19064
   330
	  | rp (DeltaEntry ds) thy = fold delta ds thy
obua@19064
   331
	and delta (Specification (names, th)) thy = 
obua@19064
   332
	    fst (SpecificationPackage.add_specification NONE names (thy,th_of thy th))
obua@19064
   333
	  | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
obua@19064
   334
	    add_hol4_mapping thyname thmname isaname thy
obua@19064
   335
	  | delta (Hol_pending (thyname, thmname, th)) thy = 
obua@19064
   336
	    add_hol4_pending thyname thmname ([], th_of thy th) thy
wenzelm@24712
   337
	  | delta (Consts cs) thy = Sign.add_consts_i cs thy
obua@19064
   338
	  | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
obua@19064
   339
	    add_hol4_const_mapping thyname constname true fullcname thy
obua@19064
   340
	  | delta (Hol_move (fullname, moved_thmname)) thy = 
obua@19064
   341
	    add_hol4_move fullname moved_thmname thy
obua@19064
   342
	  | delta (Defs (thmname, eq)) thy =
haftmann@29585
   343
	    snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
obua@19064
   344
	  | delta (Hol_theorem (thyname, thmname, th)) thy =
obua@19064
   345
	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
obua@19064
   346
	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
haftmann@28662
   347
	    snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy)
obua@19064
   348
	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
obua@19064
   349
	    add_hol4_type_mapping thyname tycname true fulltyname thy
obua@19064
   350
	  | delta (Indexed_theorem (i, th)) thy = 
obua@19064
   351
	    (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)	    	    
obua@19068
   352
          | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
obua@19068
   353
	  | delta (Dump s) thy = P.replay_add_dump s thy
obua@19064
   354
    in
obua@19064
   355
	rps
obua@19064
   356
    end
obua@19064
   357
skalberg@14516
   358
fun import_thms thyname int_thms thmnames thy =
skalberg@14516
   359
    let
obua@19064
   360
	fun zip names [] = ([], names)
obua@19064
   361
	  | zip [] _ = ([], [])
obua@19064
   362
	  | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 
obua@19064
   363
	    if thyname = thyname' andalso thmname = thmname' then
obua@19064
   364
		(if aborted then ([], thmname::names) else 
obua@19064
   365
		 let
obua@19064
   366
		     val _ = writeln ("theorem is in-sync: "^thmname)
obua@19064
   367
		     val (cached,normal) = zip names ys
obua@19064
   368
		 in
obua@19064
   369
		     (entry::cached, normal)
obua@19064
   370
		 end)
obua@19064
   371
	    else
obua@19203
   372
		let
obua@19203
   373
		    val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
obua@19203
   374
		    val _ = writeln ("proceeding with next uncached theorem...")
obua@19203
   375
		in
obua@19203
   376
		    ([], thmname::names)
obua@19203
   377
		end
obua@19203
   378
	(*	raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
obua@19064
   379
	  | zip (thmname::_) (DeltaEntry _ :: _) = 
obua@19064
   380
 	    raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
obua@19064
   381
	fun zip' xs (History ys) = 
obua@19064
   382
	    let
obua@19064
   383
		val _ = writeln ("length of xs: "^(string_of_int (length xs)))
obua@19064
   384
		val _ = writeln ("length of history: "^(string_of_int (length ys)))
obua@19064
   385
	    in
obua@19064
   386
		zip xs ys
obua@19064
   387
	    end
obua@19064
   388
	fun replay_fact thmname thy = 
skalberg@14516
   389
	    let
obua@17592
   390
		val prf = mk_proof PDisk	
obua@17594
   391
		val _ = set_disk_info_of prf thyname thmname
obua@17594
   392
                val _ = writeln ("Replaying "^thmname^" ...")
obua@17592
   393
		val p = fst (replay_proof int_thms thyname thmname prf thy)
skalberg@14516
   394
	    in
obua@17592
   395
		p
skalberg@14516
   396
	    end
obua@19064
   397
	fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
obua@19064
   398
	val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
obua@19064
   399
	val _ = ImportRecorder.set_history (History (map ThmEntry cached))
obua@19064
   400
	val res_thy = fold replay_fact normal (fold replay_cache cached thy)
skalberg@14516
   401
    in
skalberg@14516
   402
	res_thy
skalberg@14516
   403
    end
skalberg@14516
   404
skalberg@14516
   405
fun import_thm thyname thmname thy =
skalberg@14516
   406
    let
skalberg@14516
   407
	val int_thms = fst (setup_int_thms thyname thy)
skalberg@14516
   408
	fun replay_fact (thmname,thy) =
skalberg@14516
   409
	    let
obua@17592
   410
		val prf = mk_proof PDisk	
obua@17594
   411
		val _ = set_disk_info_of prf thyname thmname 	    
obua@17594
   412
                val _ = writeln ("Replaying "^thmname^" ...")
obua@17592
   413
		val p = fst (replay_proof int_thms thyname thmname prf thy)
obua@17592
   414
	    in 
obua@17592
   415
		p
skalberg@14516
   416
	    end
skalberg@14516
   417
    in
skalberg@14516
   418
	replay_fact (thmname,thy)
skalberg@14516
   419
    end
skalberg@14516
   420
wenzelm@17959
   421
end