# HG changeset patch
# User wenzelm
# Date 1005006070 -3600
# Node ID 31337dd5f5969c795756e7cd64dbf9d6e39d6b7b
# Parent  5f7f44d5e3dd92853d497f88a9c4a1fc6b49762d
tuned;

diff -r 5f7f44d5e3dd -r 31337dd5f596 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Nov 06 01:20:49 2001 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 06 01:21:10 2001 +0100
@@ -861,7 +861,7 @@
 
 (* defs *)
 
-fun cert_def ctxt eq =    (* FIXME proper treatment of extra type variables *)
+fun cert_def ctxt eq =
   let
     fun err msg = raise CONTEXT (msg ^
       "\nThe error(s) above occurred in local definition: " ^ string_of_term ctxt eq, ctxt);
@@ -873,14 +873,15 @@
       | fixed_free _ = false;
   in
     Term.dest_Free head handle TERM _ =>
-      err "Head of lhs must be a variable (free or fixed)";
+      err "Head of lhs must be a free or fixed variable";
     conditional (not (forall (fixed_free orf is_Bound) args andalso null (duplicates args)))
       (fn () => err "Arguments of lhs must be distinct variables (free or fixed)");
     conditional (head mem Term.term_frees rhs)
       (fn () => err "Element to be defined occurs on rhs");
     conditional (not (null (filter_out fixed_free (term_frees rhs) \\ args)))
-      (fn () => err "Extra free variables on rhs");
+      (fn () => err "Extra free variables on rhs");    (* FIXME show extras *)
     Term.list_all_free (mapfilter (try Term.dest_Free) args, eq)
+    (* FIXME check for extra type variables on rhs *)
   end;
 
 fun head_of_def cprop =