Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/choice_specification.ML
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
isabelle