89 val rhs' = rename_vars rhs |
89 val rhs' = rename_vars rhs |
90 |
90 |
91 val localize = instantiate ([], cvqs ~~ cqs) |
91 val localize = instantiate ([], cvqs ~~ cqs) |
92 #> fold implies_elim_swp ags |
92 #> fold implies_elim_swp ags |
93 |
93 |
94 val GI = freezeT GI |
94 val GI = Thm.freezeT GI |
95 val lGI = localize GI |
95 val lGI = localize GI |
96 |
96 |
97 val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI)) |
97 val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI)) |
98 |
98 |
99 fun mk_call_info (RIvs, RI) = |
99 fun mk_call_info (RIvs, RI) = |
100 let |
100 let |
101 fun mk_var0 (v,T) = Var ((v,0),T) |
101 fun mk_var0 (v,T) = Var ((v,0),T) |
102 |
102 |
103 val RI = freezeT RI |
103 val RI = Thm.freezeT RI |
104 val lRI = localize RI |
104 val lRI = localize RI |
105 val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI |
105 val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI |
106 val plRI = prop_of lRI |
106 val plRI = prop_of lRI |
107 val GmAs = Logic.strip_imp_prems plRI |
107 val GmAs = Logic.strip_imp_prems plRI |
108 val rcarg = case Logic.strip_imp_concl plRI of |
108 val rcarg = case Logic.strip_imp_concl plRI of |