368 |
368 |
369 val forall_elim_var = PureThy.forall_elim_var; |
369 val forall_elim_var = PureThy.forall_elim_var; |
370 val forall_elim_vars = PureThy.forall_elim_vars; |
370 val forall_elim_vars = PureThy.forall_elim_vars; |
371 |
371 |
372 fun outer_params t = |
372 fun outer_params t = |
373 let |
373 let val vs = Term.strip_all_vars t |
374 val vs = Term.strip_all_vars t; |
374 in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end; |
375 val clean_name = perhaps (try Term.dest_skolem) #> perhaps (try Term.dest_internal); |
|
376 in Term.variantlist (map (clean_name o #1) vs, []) ~~ map #2 vs end; |
|
377 |
375 |
378 (*generalize outermost parameters*) |
376 (*generalize outermost parameters*) |
379 fun gen_all th = |
377 fun gen_all th = |
380 let |
378 let |
381 val {thy, prop, maxidx, ...} = Thm.rep_thm th; |
379 val {thy, prop, maxidx, ...} = Thm.rep_thm th; |
498 in |
496 in |
499 case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of |
497 case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of |
500 [] => (fth, fn x => x) |
498 [] => (fth, fn x => x) |
501 | vars => |
499 | vars => |
502 let fun newName (Var(ix,_), (pairs,used)) = |
500 let fun newName (Var(ix,_), (pairs,used)) = |
503 let val v = variant used (string_of_indexname ix) |
501 let val v = Name.variant used (string_of_indexname ix) |
504 in ((ix,v)::pairs, v::used) end; |
502 in ((ix,v)::pairs, v::used) end; |
505 val (alist, _) = foldr newName ([], Library.foldr add_term_names |
503 val (alist, _) = foldr newName ([], Library.foldr add_term_names |
506 (prop :: Thm.terms_of_tpairs tpairs, [])) vars |
504 (prop :: Thm.terms_of_tpairs tpairs, [])) vars |
507 fun mk_inst (Var(v,T)) = |
505 fun mk_inst (Var(v,T)) = |
508 (cterm_of thy (Var(v,T)), |
506 (cterm_of thy (Var(v,T)), |