equal
deleted
inserted
replaced
255 fun globalize param_map = map_aterms |
255 fun globalize param_map = map_aterms |
256 (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) |
256 (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) |
257 | t => t); |
257 | t => t); |
258 val raw_pred = Locale.intros_of thy class |
258 val raw_pred = Locale.intros_of thy class |
259 |> fst |
259 |> fst |
260 |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of); |
260 |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); |
261 fun get_axiom thy = case (#axioms o AxClass.get_info thy) class |
261 fun get_axiom thy = case (#axioms o AxClass.get_info thy) class |
262 of [] => NONE |
262 of [] => NONE |
263 | [thm] => SOME thm; |
263 | [thm] => SOME thm; |
264 in |
264 in |
265 thy |
265 thy |