equal
deleted
inserted
replaced
88 |
88 |
89 fun add_defs defs ctxt = |
89 fun add_defs defs ctxt = |
90 let |
90 let |
91 val ((xs, mxs), specs) = defs |> split_list |>> split_list; |
91 val ((xs, mxs), specs) = defs |> split_list |>> split_list; |
92 val (bs, rhss) = specs |> split_list; |
92 val (bs, rhss) = specs |> split_list; |
93 val eqs = mk_def ctxt (xs ~~ rhss); |
93 val eqs = mk_def (Context_Position.set_visible false ctxt) (xs ~~ rhss); |
94 val lhss = map (fst o Logic.dest_equals) eqs; |
94 val lhss = map (fst o Logic.dest_equals) eqs; |
95 in |
95 in |
96 ctxt |
96 ctxt |
97 |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2 |
97 |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2 |
98 |> fold Variable.declare_term eqs |
98 |> fold Variable.declare_term eqs |