src/HOL/Tools/Function/context_tree.ML
changeset 32035 8e77b6a250d5
parent 31775 2b04504fcb69
child 33037 b22e44496dc2
     1.1 --- a/src/HOL/Tools/Function/context_tree.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -116,8 +116,9 @@
     1.4         val (c, subs) = (concl_of r, prems_of r)
     1.5  
     1.6         val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
     1.7 -       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
     1.8 -       val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
     1.9 +       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
    1.10 +       val inst = map (fn v =>
    1.11 +        (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
    1.12       in
    1.13     (cterm_instantiate inst r, dep, branches)
    1.14       end