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/Quotient/quotient_tacs.ML
changeset 59586 ddf6deaadfe8
parent 59585 68a770a8a09f
child 59621 291934bac95e 
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Mar 04 22:05:01 2015 +0100
@@ -541,7 +541,7 @@
 (* Tactic for Generalising Free Variables in a Goal *)
 
 fun inst_spec ctrm =
-  Drule.instantiate' [SOME (Thm.ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
+  Drule.instantiate' [SOME (Thm.ctyp_of_cterm ctrm)] [NONE, SOME ctrm] @{thm spec}
 
 fun inst_spec_tac ctrms =
   EVERY' (map (dtac o inst_spec) ctrms)
isabelle