src/HOL/Tools/Function/function_context_tree.ML
changeset 60781 2da59cdf531c
parent 60695 757549b4bbe6
child 60801 7664e0916eec
     1.1 --- a/src/HOL/Tools/Function/function_context_tree.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Function/function_context_tree.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -119,10 +119,10 @@
     1.4          val subst = Pattern.match thy (c, tt') (Vartab.empty, Vartab.empty)
     1.5          val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
     1.6          val inst =
     1.7 -          map (fn v => apply2 (Thm.cterm_of ctxt) (Var v, Envir.subst_term subst (Var v)))
     1.8 +          map (fn v => (#1 v, Thm.cterm_of ctxt (Envir.subst_term subst (Var v))))
     1.9              (Term.add_vars c [])
    1.10        in
    1.11 -        (cterm_instantiate inst r, dep, branches)
    1.12 +        (infer_instantiate ctxt inst r, dep, branches)
    1.13        end handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
    1.14    | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
    1.15