equal
deleted
inserted
replaced
1 (* Title: Doc/more_antiquote.ML |
1 (* Title: Doc/more_antiquote.ML |
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
2 Author: Florian Haftmann, TU Muenchen |
4 |
3 |
5 More antiquotations. |
4 More antiquotations. |
6 *) |
5 *) |
7 |
6 |
90 |
89 |
91 fun pretty_code_thm src ctxt raw_const = |
90 fun pretty_code_thm src ctxt raw_const = |
92 let |
91 let |
93 val thy = ProofContext.theory_of ctxt; |
92 val thy = ProofContext.theory_of ctxt; |
94 val const = Code_Unit.check_const thy raw_const; |
93 val const = Code_Unit.check_const thy raw_const; |
95 val (_, funcgr) = Code_Funcgr.make thy [const]; |
94 val (_, funcgr) = Code_Wellsorted.make thy [const]; |
96 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
95 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
97 val thms = Code_Funcgr.eqns funcgr const |
96 val thms = Code_Wellsorted.eqns funcgr const |
98 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
97 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
99 |> map (holize o no_vars ctxt o AxClass.overload thy); |
98 |> map (holize o no_vars ctxt o AxClass.overload thy); |
100 in ThyOutput.output_list pretty_thm src ctxt thms end; |
99 in ThyOutput.output_list pretty_thm src ctxt thms end; |
101 |
100 |
102 in |
101 in |