equal
deleted
inserted
replaced
52 |
52 |
53 fun write_file_lsetup_blk txt lthy = |
53 fun write_file_lsetup_blk txt lthy = |
54 let |
54 let |
55 val pre = implode ["\n", "local_setup ", "{", "*", "\n"] |
55 val pre = implode ["\n", "local_setup ", "{", "*", "\n"] |
56 val post = implode ["\n", "*", "}", "\n"] |
56 val post = implode ["\n", "*", "}", "\n"] |
57 val _ = write_file (enclose pre post txt) (ProofContext.theory_of lthy) |
57 val _ = write_file (enclose pre post txt) (Proof_Context.theory_of lthy) |
58 in |
58 in |
59 lthy |
59 lthy |
60 end |
60 end |
61 |
61 |
62 *} |
62 *} |