equal
deleted
inserted
replaced
81 val constT = map fastype_of result_pats ---> @{typ bool} |
81 val constT = map fastype_of result_pats ---> @{typ bool} |
82 val specialised_const = Const (constname, constT) |
82 val specialised_const = Const (constname, constT) |
83 fun specialise_intro intro = |
83 fun specialise_intro intro = |
84 (let |
84 (let |
85 val (prems, concl) = Logic.strip_horn (prop_of intro) |
85 val (prems, concl) = Logic.strip_horn (prop_of intro) |
86 val env = Pattern.unify thy |
86 val env = Pattern.unify (Context.Theory thy) |
87 (HOLogic.mk_Trueprop (list_comb (pred, pats)), concl) (Envir.empty 0) |
87 (HOLogic.mk_Trueprop (list_comb (pred, pats)), concl) (Envir.empty 0) |
88 val prems = map (Envir.norm_term env) prems |
88 val prems = map (Envir.norm_term env) prems |
89 val args = map (Envir.norm_term env) result_pats |
89 val args = map (Envir.norm_term env) result_pats |
90 val concl = HOLogic.mk_Trueprop (list_comb (specialised_const, args)) |
90 val concl = HOLogic.mk_Trueprop (list_comb (specialised_const, args)) |
91 val intro = Logic.list_implies (prems, concl) |
91 val intro = Logic.list_implies (prems, concl) |