equal
deleted
inserted
replaced
204 val _ = value_antiq "cprop" (Args.prop >> (fn t => |
204 val _ = value_antiq "cprop" (Args.prop >> (fn t => |
205 ("cprop", |
205 ("cprop", |
206 "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
206 "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
207 |
207 |
208 |
208 |
|
209 fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) => |
|
210 #1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c)) |
|
211 |> syn ? ProofContext.const_syntax_name ctxt |
|
212 |> ML_Syntax.print_string); |
|
213 |
|
214 val _ = inline_antiq "const_name" (const false); |
|
215 val _ = inline_antiq "const_syntax" (const true); |
|
216 |
|
217 |
209 |
218 |
210 (** fact references **) |
219 (** fact references **) |
211 |
220 |
212 fun thm name = ProofContext.get_thm (the_local_context ()) (Name name); |
221 fun thm name = ProofContext.get_thm (the_local_context ()) (Name name); |
213 fun thms name = ProofContext.get_thms (the_local_context ()) (Name name); |
222 fun thms name = ProofContext.get_thms (the_local_context ()) (Name name); |