equal
deleted
inserted
replaced
36 other_name_space (Method.method_space o Context.Theory)); |
36 other_name_space (Method.method_space o Context.Theory)); |
37 |
37 |
38 |
38 |
39 (* approximative syntax *) |
39 (* approximative syntax *) |
40 |
40 |
41 val get_syntax = Syntax.get_approx o Proof_Context.syn_of; |
41 val get_syntax = Syntax.get_approx o Proof_Context.syntax_of; |
42 fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type; |
42 fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type; |
43 fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const; |
43 fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const; |
44 fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed; |
44 fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed; |
45 |
45 |
46 fun get_syntax_param ctxt loc x = |
46 fun get_syntax_param ctxt loc x = |