equal
deleted
inserted
replaced
904 fun make comb = |
904 fun make comb = |
905 let |
905 let |
906 val Type ("fun", [T, T']) = fastype_of comb; |
906 val Type ("fun", [T, T']) = fastype_of comb; |
907 val (Const (case_name, _), fs) = strip_comb comb |
907 val (Const (case_name, _), fs) = strip_comb comb |
908 val used = Term.add_tfree_names comb [] |
908 val used = Term.add_tfree_names comb [] |
909 val U = TFree (Name.variant used "'t", HOLogic.typeS) |
909 val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS) |
910 val x = Free ("x", T) |
910 val x = Free ("x", T) |
911 val f = Free ("f", T' --> U) |
911 val f = Free ("f", T' --> U) |
912 fun apply_f f' = |
912 fun apply_f f' = |
913 let |
913 let |
914 val Ts = binder_types (fastype_of f') |
914 val Ts = binder_types (fastype_of f') |