equal
deleted
inserted
replaced
4 Schematic invocation of locale expression in proof context. |
4 Schematic invocation of locale expression in proof context. |
5 *) |
5 *) |
6 |
6 |
7 signature INVOKE = |
7 signature INVOKE = |
8 sig |
8 sig |
9 val invoke: string * Attrib.src list -> Locale.expr -> string option list -> |
9 val invoke: string * Attrib.src list -> Old_Locale.expr -> string option list -> |
10 (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
10 (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state |
11 val invoke_i: string * attribute list -> Locale.expr -> term option list -> |
11 val invoke_i: string * attribute list -> Old_Locale.expr -> term option list -> |
12 (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state |
12 (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state |
13 end; |
13 end; |
14 |
14 |
15 structure Invoke: INVOKE = |
15 structure Invoke: INVOKE = |
16 struct |
16 struct |
102 end; |
102 end; |
103 |
103 |
104 in |
104 in |
105 |
105 |
106 fun invoke x = |
106 fun invoke x = |
107 gen_invoke Attrib.attribute Locale.read_expr Syntax.parse_term ProofContext.add_fixes x; |
107 gen_invoke Attrib.attribute Old_Locale.read_expr Syntax.parse_term ProofContext.add_fixes x; |
108 fun invoke_i x = gen_invoke (K I) Locale.cert_expr (K I) ProofContext.add_fixes_i x; |
108 fun invoke_i x = gen_invoke (K I) Old_Locale.cert_expr (K I) ProofContext.add_fixes_i x; |
109 |
109 |
110 end; |
110 end; |
111 |
111 |
112 |
112 |
113 (* concrete syntax *) |
113 (* concrete syntax *) |