equal
deleted
inserted
replaced
290 fun inst_thms thy = |
290 fun inst_thms thy = |
291 Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) []; |
291 Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) []; |
292 |
292 |
293 fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts); |
293 fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts); |
294 |
294 |
295 fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy); |
295 fun unoverload thy = rewrite_rule (inst_thms thy); |
296 fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy)); |
296 fun overload thy = rewrite_rule (map Thm.symmetric (inst_thms thy)); |
297 |
297 |
298 fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy); |
298 fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy); |
299 fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy)); |
299 fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy)); |
300 |
300 |
301 fun lookup_inst_param consts params (c, T) = |
301 fun lookup_inst_param consts params (c, T) = |