equal
deleted
inserted
replaced
9 signature PROOF_CONTEXT = |
9 signature PROOF_CONTEXT = |
10 sig |
10 sig |
11 val theory_of: Proof.context -> theory |
11 val theory_of: Proof.context -> theory |
12 val init_global: theory -> Proof.context |
12 val init_global: theory -> Proof.context |
13 val get_global: theory -> string -> Proof.context |
13 val get_global: theory -> string -> Proof.context |
14 val cterm_of: Proof.context -> term -> cterm |
|
15 val ctyp_of: Proof.context -> typ -> ctyp |
|
16 type mode |
14 type mode |
17 val mode_default: mode |
15 val mode_default: mode |
18 val mode_stmt: mode |
16 val mode_stmt: mode |
19 val mode_pattern: mode |
17 val mode_pattern: mode |
20 val mode_schematic: mode |
18 val mode_schematic: mode |
180 |
178 |
181 val theory_of = Proof_Context.theory_of; |
179 val theory_of = Proof_Context.theory_of; |
182 val init_global = Proof_Context.init_global; |
180 val init_global = Proof_Context.init_global; |
183 val get_global = Proof_Context.get_global; |
181 val get_global = Proof_Context.get_global; |
184 |
182 |
185 val cterm_of = Thm.cterm_of o theory_of; |
|
186 val ctyp_of = Thm.ctyp_of o theory_of; |
|
187 |
|
188 |
183 |
189 |
184 |
190 (** inner syntax mode **) |
185 (** inner syntax mode **) |
191 |
186 |
192 datatype mode = |
187 datatype mode = |
1167 fun gen_assms prepp exp args ctxt = |
1162 fun gen_assms prepp exp args ctxt = |
1168 let |
1163 let |
1169 val ((propss, _), ctxt1) = prepp (map snd args) ctxt; |
1164 val ((propss, _), ctxt1) = prepp (map snd args) ctxt; |
1170 val _ = Variable.warn_extra_tfrees ctxt ctxt1; |
1165 val _ = Variable.warn_extra_tfrees ctxt ctxt1; |
1171 val (premss, ctxt2) = |
1166 val (premss, ctxt2) = |
1172 fold_burrow (Assumption.add_assms exp o map (cterm_of ctxt)) propss ctxt1; |
1167 fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss ctxt1; |
1173 in |
1168 in |
1174 ctxt2 |
1169 ctxt2 |
1175 |> auto_bind_facts (flat propss) |
1170 |> auto_bind_facts (flat propss) |
1176 |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss) |
1171 |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss) |
1177 end; |
1172 end; |