src/HOL/Tools/Function/context_tree.ML

 
        val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
        val (c, subs) = (concl_of r, prems_of r)
 
        val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
-       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
-       val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
+       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
+       val inst = map (fn v =>
+        (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
      in
    (cterm_instantiate inst r, dep, branches)
      end
     handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
   | find_cong_rule _ _ _ [] _ = sys_error "Function/context_tree.ML: No cong rule found!"