added @{const_name}, @{const_syntax};
authorwenzelm
Wed Feb 28 22:05:41 2007 +0100 (2007-02-28)
changeset 22376b711c2ad7507
parent 22375 823f7bee42df
child 22377 61610b1beedf
added @{const_name}, @{const_syntax};
NEWS
src/Pure/Thy/ml_context.ML
     1.1 --- a/NEWS	Wed Feb 28 16:35:00 2007 +0100
     1.2 +++ b/NEWS	Wed Feb 28 22:05:41 2007 +0100
     1.3 @@ -769,6 +769,8 @@
     1.4  ML {* @{cprop "x == y"} *}
     1.5  ML {* @{thm asm_rl} *}
     1.6  ML {* @{thms asm_rl} *}
     1.7 +ML {* @{const_name c} *}
     1.8 +ML {* @{const_syntax c} *}
     1.9  ML {* @{context} *}
    1.10  ML {* @{theory} *}
    1.11  ML {* @{theory Pure} *}
     2.1 --- a/src/Pure/Thy/ml_context.ML	Wed Feb 28 16:35:00 2007 +0100
     2.2 +++ b/src/Pure/Thy/ml_context.ML	Wed Feb 28 22:05:41 2007 +0100
     2.3 @@ -206,6 +206,15 @@
     2.4      "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
     2.5  
     2.6  
     2.7 +fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
     2.8 +  #1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c))
     2.9 +  |> syn ? ProofContext.const_syntax_name ctxt
    2.10 +  |> ML_Syntax.print_string);
    2.11 +
    2.12 +val _ = inline_antiq "const_name" (const false);
    2.13 +val _ = inline_antiq "const_syntax" (const true);
    2.14 +
    2.15 +
    2.16  
    2.17  (** fact references **)
    2.18