changeset 59586 | ddf6deaadfe8 |
parent 59582 | 0fbed69ff081 |
child 59621 | 291934bac95e |
--- a/src/HOL/Tools/choice_specification.ML Wed Mar 04 20:50:20 2015 +0100 +++ b/src/HOL/Tools/choice_specification.ML Wed Mar 04 22:05:01 2015 +0100 @@ -137,7 +137,7 @@ fun inst_all thy v thm = let val cv = Thm.cterm_of thy v - val cT = Thm.ctyp_of_term cv + val cT = Thm.ctyp_of_cterm cv val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec in thm RS spec' end fun remove_alls frees thm = fold (inst_all (Thm.theory_of_thm thm)) frees thm