66 |
66 |
67 structure Generic_Target: GENERIC_TARGET = |
67 structure Generic_Target: GENERIC_TARGET = |
68 struct |
68 struct |
69 |
69 |
70 (** consts **) |
70 (** consts **) |
|
71 |
|
72 fun export_abbrev lthy preprocess (b, rhs) = |
|
73 let |
|
74 val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); |
|
75 |
|
76 val rhs' = rhs |
|
77 |> Assumption.export_term lthy (Local_Theory.target_of lthy) |
|
78 |> preprocess; |
|
79 val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' [])); |
|
80 val u = fold_rev lambda term_params rhs'; |
|
81 val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; |
|
82 |
|
83 val extra_tfrees = |
|
84 subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []); |
|
85 val type_params = map (Logic.mk_type o TFree) extra_tfrees; |
|
86 in ((b, global_rhs), (extra_tfrees, (type_params, term_params))) end; |
71 |
87 |
72 fun check_mixfix ctxt (b, extra_tfrees) mx = |
88 fun check_mixfix ctxt (b, extra_tfrees) mx = |
73 if null extra_tfrees then mx |
89 if null extra_tfrees then mx |
74 else |
90 else |
75 (if Context_Position.is_visible ctxt then |
91 (if Context_Position.is_visible ctxt then |
282 |
298 |
283 (* abbrev *) |
299 (* abbrev *) |
284 |
300 |
285 fun abbrev target_abbrev prmode ((b, mx), rhs) lthy = |
301 fun abbrev target_abbrev prmode ((b, mx), rhs) lthy = |
286 let |
302 let |
287 val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); |
303 val ((b, global_rhs), (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I (b, rhs); |
288 |
|
289 val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs; |
|
290 val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' [])); |
|
291 val u = fold_rev lambda term_params rhs'; |
|
292 val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; |
|
293 |
|
294 val extra_tfrees = |
|
295 subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []); |
|
296 val mx' = check_mixfix lthy (b, extra_tfrees) mx; |
304 val mx' = check_mixfix lthy (b, extra_tfrees) mx; |
297 val type_params = map (Logic.mk_type o TFree) extra_tfrees; |
|
298 in |
305 in |
299 lthy |
306 lthy |
300 |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params) |
307 |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params) |
301 |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd |
308 |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd |
302 |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs) |
309 |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs) |