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/Provers/splitter.ML
changeset 10403 2955ee2424ce
parent 10034 4bca6b2d2589
child 10411 c7375583fe4e 
--- a/src/Provers/splitter.ML	Mon Nov 06 22:49:16 2000 +0100
+++ b/src/Provers/splitter.ML	Mon Nov 06 22:50:01 2000 +0100
@@ -208,7 +208,7 @@
               Const(c, cT) =>
                 let fun find [] = []
                       | find ((gcT, thm, T, n)::tups) =
-                          if Type.typ_instance(Sign.tsig_of sg, cT, gcT)
+                          if Sign.typ_instance sg (cT, gcT)
                           then
                             let val t2 = list_comb (h, take (n, ts))
                             in mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
isabelle