equal
deleted
inserted
replaced
84 val bvs = map_index (Bound o fst) ps; |
84 val bvs = map_index (Bound o fst) ps; |
85 (* select variables of the right class *) |
85 (* select variables of the right class *) |
86 val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t))) |
86 val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t))) |
87 (term_frees goal @ bvs); |
87 (term_frees goal @ bvs); |
88 (* build the tuple *) |
88 (* build the tuple *) |
89 val s = Library.foldr1 (fn (v, s) => |
89 val s = (Library.foldr1 (fn (v, s) => |
90 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) |
90 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ; |
91 vs; |
|
92 val fs_name_thm = get_dyn_thm thy ("fs_"^atom_basename^"1") atom_basename; |
91 val fs_name_thm = get_dyn_thm thy ("fs_"^atom_basename^"1") atom_basename; |
93 val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; |
92 val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; |
94 val exists_fresh' = at_name_inst_thm RS at_exists_fresh'; |
93 val exists_fresh' = at_name_inst_thm RS at_exists_fresh'; |
95 (* find the variable we want to instantiate *) |
94 (* find the variable we want to instantiate *) |
96 val x = hd (term_vars (prop_of exists_fresh')); |
95 val x = hd (term_vars (prop_of exists_fresh')); |