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/Function/function_elims.ML
changeset 55968 94242fa87638
parent 54739 d41099c829bf
child 58963 26bf09b95dda 
--- a/src/HOL/Tools/Function/function_elims.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/Function/function_elims.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -114,7 +114,7 @@
         val args = HOLogic.mk_tuple arg_vars;
         val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
 
-        val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
+        val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
 
         val cprop = cert prop;
 
@@ -155,4 +155,3 @@
 end;
 
 end;
-
isabelle