equal
deleted
inserted
replaced
242 fun define_const internal fp_b version name rhs lthy = |
242 fun define_const internal fp_b version name rhs lthy = |
243 let |
243 let |
244 val b = mk_version_fp_binding internal lthy version fp_b name; |
244 val b = mk_version_fp_binding internal lthy version fp_b name; |
245 |
245 |
246 val ((free, (_, def_free)), (lthy, lthy_old)) = lthy |
246 val ((free, (_, def_free)), (lthy, lthy_old)) = lthy |
247 |> Local_Theory.open_target |> snd |
247 |> Local_Theory.open_target |
248 |> Local_Theory.define ((b, NoSyn), ((Thm.def_binding b |> Binding.concealed, []), rhs)) |
248 |> Local_Theory.define ((b, NoSyn), ((Thm.def_binding b |> Binding.concealed, []), rhs)) |
249 ||> `Local_Theory.close_target; |
249 ||> `Local_Theory.close_target; |
250 |
250 |
251 val phi = Proof_Context.export_morphism lthy_old lthy; |
251 val phi = Proof_Context.export_morphism lthy_old lthy; |
252 |
252 |
257 end; |
257 end; |
258 |
258 |
259 fun define_single_primrec b eqs lthy = |
259 fun define_single_primrec b eqs lthy = |
260 let |
260 let |
261 val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy |
261 val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy |
262 |> Local_Theory.open_target |> snd |
262 |> Local_Theory.open_target |
263 |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*) |
263 |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*) |
264 |> primrec false [] [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs) |
264 |> primrec false [] [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs) |
265 ||> `Local_Theory.close_target; |
265 ||> `Local_Theory.close_target; |
266 |
266 |
267 val phi = Proof_Context.export_morphism lthy_old lthy; |
267 val phi = Proof_Context.export_morphism lthy_old lthy; |
539 let |
539 let |
540 val T_b = mk_version_fp_binding_ugly true lthy version fp_b sigN; |
540 val T_b = mk_version_fp_binding_ugly true lthy version fp_b sigN; |
541 val ctr_b = mk_version_fp_binding false lthy version fp_b SigN; |
541 val ctr_b = mk_version_fp_binding false lthy version fp_b SigN; |
542 val sel_b = mk_version_fp_binding true lthy version fp_b unsigN; |
542 val sel_b = mk_version_fp_binding true lthy version fp_b unsigN; |
543 |
543 |
544 val lthy = Local_Theory.open_target lthy |> snd; |
544 val lthy = Local_Theory.open_target lthy; |
545 |
545 |
546 val T_name = Local_Theory.full_name lthy T_b; |
546 val T_name = Local_Theory.full_name lthy T_b; |
547 |
547 |
548 val tyargs = map2 (fn alive => fn T => |
548 val tyargs = map2 (fn alive => fn T => |
549 (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T))) |
549 (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T))) |
572 val T_b = Binding.prefix_name s_prefix sig_T_b; |
572 val T_b = Binding.prefix_name s_prefix sig_T_b; |
573 val Oper_b = mk_version_fp_binding false lthy version fp_b OperN; |
573 val Oper_b = mk_version_fp_binding false lthy version fp_b OperN; |
574 val VLeaf_b = mk_version_fp_binding false lthy version fp_b VLeafN; |
574 val VLeaf_b = mk_version_fp_binding false lthy version fp_b VLeafN; |
575 val CLeaf_b = mk_version_fp_binding false lthy version fp_b CLeafN; |
575 val CLeaf_b = mk_version_fp_binding false lthy version fp_b CLeafN; |
576 |
576 |
577 val lthy = Local_Theory.open_target lthy |> snd; |
577 val lthy = Local_Theory.open_target lthy; |
578 |
578 |
579 val sig_T_name = Local_Theory.full_name lthy sig_T_b; |
579 val sig_T_name = Local_Theory.full_name lthy sig_T_b; |
580 val T_name = Long_Name.map_base_name (prefix s_prefix) sig_T_name; |
580 val T_name = Long_Name.map_base_name (prefix s_prefix) sig_T_name; |
581 |
581 |
582 val As = Es @ [Y]; |
582 val As = Es @ [Y]; |