equal
deleted
inserted
replaced
86 |
86 |
87 fun pretty_code_thm src ctxt raw_const = |
87 fun pretty_code_thm src ctxt raw_const = |
88 let |
88 let |
89 val thy = ProofContext.theory_of ctxt; |
89 val thy = ProofContext.theory_of ctxt; |
90 val const = Code_Unit.check_const thy raw_const; |
90 val const = Code_Unit.check_const thy raw_const; |
91 val (_, funcgr) = Code_Wellsorted.make thy [const]; |
91 val (_, funcgr) = Code_Wellsorted.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_Wellsorted.eqns funcgr const |
93 val thms = Code_Wellsorted.eqns funcgr const |
94 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
94 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
95 |> map (holize o no_vars ctxt o AxClass.overload thy); |
95 |> map (holize o no_vars ctxt o AxClass.overload thy); |
96 in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end; |
96 in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end; |