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_core.ML
changeset 55990 41c6b99c5fb7
parent 55396 91bc9f69a958
child 58634 9f10d82e8188 
--- a/src/HOL/Tools/Function/function_core.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -366,7 +366,7 @@
     val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 
     val exactly_one =
-      ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+      @{thm ex1I} |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
       |> curry (op COMP) existence
       |> curry (op COMP) uniqueness
       |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
isabelle