1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Thu May 10 00:39:48 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu May 10 00:39:49 2007 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4        val inst_morph = lift_morphism thy o Thm.instantiate 
     1.5  
     1.6        fun match data = 
     1.7 -          SOME (morph_fundef_data (inst_morph (Thm.cterm_match (cterm_of thy (fst data), ct))) (snd data))
     1.8 +          SOME (morph_fundef_data (inst_morph (Thm.match (cterm_of thy (fst data), ct))) (snd data))
     1.9            handle Pattern.MATCH => NONE
    1.10      in 
    1.11        get_first match (NetRules.retrieve (FundefData.get ctxt) t)