tuned;

--- a/src/Pure/Isar/term_style.ML	Thu Apr 27 15:06:42 2006 +0200
+++ b/src/Pure/Isar/term_style.ML	Thu Apr 27 15:06:42 2006 +0200
@@ -62,7 +62,7 @@
 
 fun style_parm_premise i ctxt t =
   let val prems = Logic.strip_imp_prems t in
-    if i <= length prems then List.nth (prems, i - 1)
+    if i <= length prems then nth prems (i - 1)
     else error ("Not enough premises for prem" ^ string_of_int i ^
       " in propositon: " ^ ProofContext.string_of_term ctxt t)
   end;

--- a/src/Pure/Syntax/ast.ML	Thu Apr 27 15:06:42 2006 +0200
+++ b/src/Pure/Syntax/ast.ML	Thu Apr 27 15:06:42 2006 +0200
@@ -98,23 +98,16 @@
 
 (** check translation rules **)
 
-(*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions:
-   - the lhs has unique vars,
-   - vars of rhs is subset of vars of lhs*)
-
 fun rule_error (rule as (lhs, rhs)) =
   let
-    fun vars_of (Constant _) = []
-      | vars_of (Variable x) = [x]
-      | vars_of (Appl asts) = List.concat (map vars_of asts);
+    fun add_vars (Constant _) = I
+      | add_vars (Variable x) = cons x
+      | add_vars (Appl asts) = fold add_vars asts;
 
-    fun unique (x :: xs) = not (x mem xs) andalso unique xs
-      | unique [] = true;
-
-    val lvars = vars_of lhs;
-    val rvars = vars_of rhs;
+    val lvars = add_vars lhs [];
+    val rvars = add_vars rhs [];
   in
-    if not (unique lvars) then SOME "duplicate vars in lhs"
+    if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
     else if not (rvars subset lvars) then SOME "rhs contains extra variables"
     else NONE
   end;