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/Meson/meson_clausify.ML
changeset 59586 ddf6deaadfe8
parent 59582 0fbed69ff081
child 59621 291934bac95e 
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Mar 04 22:05:01 2015 +0100
@@ -103,7 +103,7 @@
   let
       val thy = Thm.theory_of_cterm ct
       val Abs(x,_,body) = Thm.term_of ct
-      val Type(@{type_name fun}, [xT,bodyT]) = Thm.typ_of (Thm.ctyp_of_term ct)
+      val Type (@{type_name fun}, [xT,bodyT]) = Thm.typ_of_cterm ct
       val cxT = Thm.ctyp_of thy xT
       val cbodyT = Thm.ctyp_of thy bodyT
       fun makeK () =
isabelle