# HG changeset patch # User wenzelm # Date 1148425501 -7200 # Node ID 0e7e236fab5067bc677e208fad2cfeabfbacce47 # Parent 246afe8852bc23febb0ab418af171481e1dbb9fe tuned; diff -r 246afe8852bc -r 0e7e236fab50 src/Pure/defs.ML --- a/src/Pure/defs.ML Wed May 24 01:04:59 2006 +0200 +++ b/src/Pure/defs.ML Wed May 24 01:05:01 2006 +0200 @@ -36,6 +36,9 @@ else [Pretty.list "(" ")" (map (Pretty.typ pp o Type.freeze_type) args)]; in Pretty.block (Pretty.str c :: prt_args) end; +fun plain_args args = + forall Term.is_TVar args andalso not (has_duplicates (op =) args); + fun disjoint_args (Ts, Us) = not (Type.could_unifys (Ts, Us)) orelse ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false) @@ -198,9 +201,6 @@ (* define *) -fun plain_args args = - forall Term.is_TVar args andalso not (has_duplicates (op =) args); - fun define pp consts unchecked is_def module name lhs rhs (Defs defs) = let fun typargs const = (#1 const, Consts.typargs consts const);