# 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);