equal
deleted
inserted
replaced
120 val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; |
120 val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else []; |
121 |
121 |
122 (*obtain vars*) |
122 (*obtain vars*) |
123 val (vars, vars_ctxt) = prep_vars raw_vars ctxt; |
123 val (vars, vars_ctxt) = prep_vars raw_vars ctxt; |
124 val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
124 val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
125 val xs = map (Name.name_of o #1) vars; |
125 val xs = map (Binding.base_name o #1) vars; |
126 |
126 |
127 (*obtain asms*) |
127 (*obtain asms*) |
128 val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); |
128 val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); |
129 val asm_props = maps (map fst) proppss; |
129 val asm_props = maps (map fst) proppss; |
130 val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; |
130 val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; |
259 val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule'; |
259 val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule'; |
260 in ((vars', rule''), ctxt') end; |
260 in ((vars', rule''), ctxt') end; |
261 |
261 |
262 fun inferred_type (binding, _, mx) ctxt = |
262 fun inferred_type (binding, _, mx) ctxt = |
263 let |
263 let |
264 val x = Name.name_of binding; |
264 val x = Binding.base_name binding; |
265 val (T, ctxt') = ProofContext.inferred_param x ctxt |
265 val (T, ctxt') = ProofContext.inferred_param x ctxt |
266 in ((x, T, mx), ctxt') end; |
266 in ((x, T, mx), ctxt') end; |
267 |
267 |
268 fun polymorphic ctxt vars = |
268 fun polymorphic ctxt vars = |
269 let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) |
269 let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars)) |