equal
deleted
inserted
replaced
317 |
317 |
318 local |
318 local |
319 |
319 |
320 fun inst_proof mk_prop add_thms inst int theory = |
320 fun inst_proof mk_prop add_thms inst int theory = |
321 theory |
321 theory |
322 |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard |
322 |> IsarThy.multi_theorem_i Drule.internalK (K I) ProofContext.export_standard |
323 ("", [fn (thy, th) => (add_thms [th] thy, th)]) [] |
323 ("", [fn (thy, th) => (add_thms [th] thy, th)]) [] |
324 (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int; |
324 (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int; |
325 |
325 |
326 in |
326 in |
327 |
327 |