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/Import/shuffler.ML
changeset 31945 d5f186aa0bed
parent 31244 4ed31c673baf
child 32091 30e2ffbba718 
--- a/src/HOL/Import/shuffler.ML	Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/Import/shuffler.ML	Mon Jul 06 21:24:30 2009 +0200
@@ -595,7 +595,7 @@
                 val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
                 val triv_th = trivial rhs
                 val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
-                val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
+                val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
                                  SOME(th,_) => SOME th
                                | NONE => NONE
             in
isabelle