equal
deleted
inserted
replaced
65 |> Context.theory_map; |
65 |> Context.theory_map; |
66 |
66 |
67 fun local_setup source = |
67 fun local_setup source = |
68 ML_Lex.read_source false source |
68 ML_Lex.read_source false source |
69 |> ML_Context.expression (#range source) |
69 |> ML_Context.expression (#range source) |
70 "val setup: local_theory -> local_theory" "Context.map_proof setup" |
70 "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup" |
71 |> Context.proof_map; |
71 |> Context.proof_map; |
72 |
72 |
73 |
73 |
74 (* translation functions *) |
74 (* translation functions *) |
75 |
75 |