equal
deleted
inserted
replaced
255 val ctypify = Thm.ctyp_of sgn |
255 val ctypify = Thm.ctyp_of sgn |
256 val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); |
256 val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); |
257 val prop = (Thm.prop_of th); |
257 val prop = (Thm.prop_of th); |
258 val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs); |
258 val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs); |
259 val ctyfixes = |
259 val ctyfixes = |
260 Library.mapfilter |
260 map_filter |
261 (fn (v as ((s,i),ty)) => |
261 (fn (v as ((s,i),ty)) => |
262 if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty))) |
262 if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty))) |
263 else NONE) tvars; |
263 else NONE) tvars; |
264 in Thm.instantiate (ctyfixes, []) th end; |
264 in Thm.instantiate (ctyfixes, []) th end; |
265 fun fix_vars_upto_idx ix th = |
265 fun fix_vars_upto_idx ix th = |
269 val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); |
269 val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); |
270 val prop = (Thm.prop_of th); |
270 val prop = (Thm.prop_of th); |
271 val vars = map Term.dest_Var (List.foldr Term.add_term_vars |
271 val vars = map Term.dest_Var (List.foldr Term.add_term_vars |
272 [] (prop :: tpairs)); |
272 [] (prop :: tpairs)); |
273 val cfixes = |
273 val cfixes = |
274 Library.mapfilter |
274 map_filter |
275 (fn (v as ((s,i),ty)) => |
275 (fn (v as ((s,i),ty)) => |
276 if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty))) |
276 if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty))) |
277 else NONE) vars; |
277 else NONE) vars; |
278 in Thm.instantiate ([], cfixes) th end; |
278 in Thm.instantiate ([], cfixes) th end; |
279 |
279 |