equal
deleted
inserted
replaced
320 fun inst_thms thy = |
320 fun inst_thms thy = |
321 Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) []; |
321 Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) []; |
322 |
322 |
323 fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts); |
323 fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts); |
324 |
324 |
325 fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy); |
325 fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy); |
326 fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy)); |
326 fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy)); |
327 |
327 |
328 fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy); |
328 fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy); |
329 fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy)); |
329 fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy)); |
330 |
330 |
331 fun lookup_inst_param consts params (c, T) = |
331 fun lookup_inst_param consts params (c, T) = |
332 (case get_inst_tyco consts (c, T) of |
332 (case get_inst_tyco consts (c, T) of |
333 SOME tyco => AList.lookup (op =) params (c, tyco) |
333 SOME tyco => AList.lookup (op =) params (c, tyco) |
334 | NONE => NONE); |
334 | NONE => NONE); |