equal
deleted
inserted
replaced
79 List.partition (fn (((x, _) : indexname), _) => String.isPrefix "'" x) insts; |
79 List.partition (fn (((x, _) : indexname), _) => String.isPrefix "'" x) insts; |
80 |
80 |
81 val ctxt1 = |
81 val ctxt1 = |
82 ctxt |
82 ctxt |
83 |> Context_Position.not_really |
83 |> Context_Position.not_really |
84 |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2; |
84 |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2; |
85 |
85 |
86 val typs = |
86 val typs = |
87 map snd type_insts |
87 map snd type_insts |
88 |> Syntax.read_typs ctxt1 |
88 |> Syntax.read_typs ctxt1 |
89 |> Syntax.check_typs ctxt1; |
89 |> Syntax.check_typs ctxt1; |
142 |
142 |
143 fun close_unchecked_insts context ((insts,concl_inst), fixes) = |
143 fun close_unchecked_insts context ((insts,concl_inst), fixes) = |
144 let |
144 let |
145 val ctxt = Context.proof_of context; |
145 val ctxt = Context.proof_of context; |
146 val ctxt1 = ctxt |
146 val ctxt1 = ctxt |
147 |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2; |
147 |> fold_map Proof_Context.read_var fixes |-> Proof_Context.add_fixes |> #2; |
148 |
148 |
149 val insts' = insts @ concl_inst; |
149 val insts' = insts @ concl_inst; |
150 |
150 |
151 val term_insts = |
151 val term_insts = |
152 map (the_list o (Option.map Parse_Tools.the_parse_val)) insts' |
152 map (the_list o (Option.map Parse_Tools.the_parse_val)) insts' |