equal
deleted
inserted
replaced
89 val thy = ProofContext.theory_of ctxt; |
89 val thy = ProofContext.theory_of ctxt; |
90 val const = Code.check_const thy raw_const; |
90 val const = Code.check_const thy raw_const; |
91 val (_, eqngr) = Code_Preproc.obtain thy [const] []; |
91 val (_, eqngr) = Code_Preproc.obtain thy [const] []; |
92 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
92 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
93 val thms = Code_Preproc.cert eqngr const |
93 val thms = Code_Preproc.cert eqngr const |
94 |> Code.equations_thms_cert thy |
94 |> Code.equations_of_cert thy |
95 |> snd |
95 |> snd |
96 |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE) |
96 |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
97 |> map (holize o no_vars ctxt o AxClass.overload thy); |
97 |> map (holize o no_vars ctxt o AxClass.overload thy); |
98 in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end; |
98 in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end; |
99 |
99 |
100 in |
100 in |
101 |
101 |