Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thm.match;
authorwenzelm
Thu, 10 May 2007 00:39:49 +0200
changeset 22903 95ad1a91ecef
parent 22902 ac833b4bb7ee
child 22904 de2d630e1548
Thm.match;
src/HOL/Tools/function_package/fundef_common.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu May 10 00:39:48 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu May 10 00:39:49 2007 +0200
@@ -113,7 +113,7 @@
       val inst_morph = lift_morphism thy o Thm.instantiate 
 
       fun match data = 
-          SOME (morph_fundef_data (inst_morph (Thm.cterm_match (cterm_of thy (fst data), ct))) (snd data))
+          SOME (morph_fundef_data (inst_morph (Thm.match (cterm_of thy (fst data), ct))) (snd data))
           handle Pattern.MATCH => NONE
     in 
       get_first match (NetRules.retrieve (FundefData.get ctxt) t)
isabelle