equal
deleted
inserted
replaced
202 |
202 |
203 |
203 |
204 (* notation *) |
204 (* notation *) |
205 |
205 |
206 fun gen_notation prep_const add mode args lthy = |
206 fun gen_notation prep_const add mode args lthy = |
207 lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args); |
207 let |
|
208 val ctxt = ProofContext.set_mode ProofContext.mode_abbrev lthy; |
|
209 fun prep_arg (s, mx) = |
|
210 let |
|
211 val t = Syntax.check_term ctxt |
|
212 (case prep_const ctxt s of Const (c, _) => Const (c, dummyT) | a => a); |
|
213 val [t'] = Syntax.uncheck_terms ctxt [t]; |
|
214 val u = if Term.is_Const t' orelse Term.is_Free t' then t' else t; |
|
215 in (u, mx) end; |
|
216 in lthy |> LocalTheory.notation add mode (map prep_arg args) end; |
208 |
217 |
209 val notation = gen_notation (K I); |
218 val notation = gen_notation (K I); |
210 val notation_cmd = gen_notation ProofContext.read_const; |
219 val notation_cmd = gen_notation ProofContext.read_const; |
211 |
220 |
212 |
221 |