723 fun add_defs def_insts = |
723 fun add_defs def_insts = |
724 let |
724 let |
725 fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt) |
725 fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt) |
726 | add (SOME (SOME x, (t, _))) ctxt = |
726 | add (SOME (SOME x, (t, _))) ctxt = |
727 let val ([(lhs, (_, th))], ctxt') = |
727 let val ([(lhs, (_, th))], ctxt') = |
728 Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt |
728 Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt |
729 in ((SOME lhs, [th]), ctxt') end |
729 in ((SOME lhs, [th]), ctxt') end |
730 | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt) |
730 | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt) |
731 | add (SOME (NONE, (t, _))) ctxt = |
731 | add (SOME (NONE, (t, _))) ctxt = |
732 let |
732 let |
733 val (s, _) = Name.variant "x" (Variable.names_of ctxt); |
733 val (s, _) = Name.variant "x" (Variable.names_of ctxt); |
734 val x = Binding.name s; |
734 val x = Binding.name s; |
735 val ([(lhs, (_, th))], ctxt') = ctxt |
735 val ([(lhs, (_, th))], ctxt') = ctxt |
736 |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))]; |
736 |> Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))]; |
737 in ((SOME lhs, [th]), ctxt') end |
737 in ((SOME lhs, [th]), ctxt') end |
738 | add NONE ctxt = ((NONE, []), ctxt); |
738 | add NONE ctxt = ((NONE, []), ctxt); |
739 in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; |
739 in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; |
740 |
740 |
741 |
741 |