src/Pure/defs.ML
changeset 19707 0e7e236fab50
parent 19701 c07c31ac689b
child 19712 3ae3cc4b1eac
     1.1 --- a/src/Pure/defs.ML	Wed May 24 01:04:59 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Wed May 24 01:05:01 2006 +0200
     1.3 @@ -36,6 +36,9 @@
     1.4        else [Pretty.list "(" ")" (map (Pretty.typ pp o Type.freeze_type) args)];
     1.5    in Pretty.block (Pretty.str c :: prt_args) end;
     1.6  
     1.7 +fun plain_args args =
     1.8 +  forall Term.is_TVar args andalso not (has_duplicates (op =) args);
     1.9 +
    1.10  fun disjoint_args (Ts, Us) =
    1.11    not (Type.could_unifys (Ts, Us)) orelse
    1.12      ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
    1.13 @@ -198,9 +201,6 @@
    1.14  
    1.15  (* define *)
    1.16  
    1.17 -fun plain_args args =
    1.18 -  forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    1.19 -
    1.20  fun define pp consts unchecked is_def module name lhs rhs (Defs defs) =
    1.21    let
    1.22      fun typargs const = (#1 const, Consts.typargs consts const);