equal
deleted
inserted
replaced
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 (Code_Preproc.preprocess_functrans thy) c |
46 val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c |
47 |> Code.equations_thms_cert thy |
47 |> Code.bare_thms_of_cert thy |
48 |> snd |
|
49 |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE) |
|
50 |> map (AxClass.overload thy) |
48 |> map (AxClass.overload thy) |
51 |> filter (is_instance T o snd o const_of o prop_of); |
49 |> filter (is_instance T o snd o const_of o prop_of); |
52 val module_name = case Symtab.lookup (ModuleData.get thy) c |
50 val module_name = case Symtab.lookup (ModuleData.get thy) c |
53 of SOME module_name => module_name |
51 of SOME module_name => module_name |
54 | NONE => case get_defn thy defs c T |
52 | NONE => case get_defn thy defs c T |