equal
deleted
inserted
replaced
57 val thms = Code.these_raw_eqns thy c' |
57 val thms = Code.these_raw_eqns thy c' |
58 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
58 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
59 |> expand_eta thy |
59 |> expand_eta thy |
60 |> map (AxClass.overload thy) |
60 |> map (AxClass.overload thy) |
61 |> map_filter (meta_eq_to_obj_eq thy) |
61 |> map_filter (meta_eq_to_obj_eq thy) |
62 |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var |
62 |> Code_Unit.norm_varnames thy |
63 |> map (rpair opt_name) |
63 |> map (rpair opt_name) |
64 in if null thms then NONE else SOME thms end; |
64 in if null thms then NONE else SOME thms end; |
65 |
65 |
66 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; |
66 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; |
67 val const_of = dest_Const o head_of o fst o dest_eqn; |
67 val const_of = dest_Const o head_of o fst o dest_eqn; |