equal
deleted
inserted
replaced
41 | avoid_value thy thms = thms; |
41 | avoid_value thy thms = thms; |
42 |
42 |
43 fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else |
43 fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else |
44 let |
44 let |
45 val c = AxClass.unoverload_const thy (raw_c, T); |
45 val c = AxClass.unoverload_const thy (raw_c, T); |
46 val raw_thms = Code.get_cert thy I c |
46 val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c |
47 |> Code.eqns_of_cert thy |
47 |> Code.eqns_of_cert thy |
48 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
48 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
49 |> map (AxClass.overload thy) |
49 |> map (AxClass.overload thy) |
50 |> filter (is_instance T o snd o const_of o prop_of); |
50 |> filter (is_instance T o snd o const_of o prop_of); |
51 val module_name = case Symtab.lookup (ModuleData.get thy) c |
51 val module_name = case Symtab.lookup (ModuleData.get thy) c |