# HG changeset patch
# User berghofe
# Date 1062684255 -7200
# Node ID 2e0e02d68cbb86ec4fc8b2c7056335fc086d9196
# Parent  466a2a69e7e8e2bd967dee1dfb7b89d74465dece
Changed no_vars such that it outputs list of illegal schematic variables.

diff -r 466a2a69e7e8 -r 2e0e02d68cbb src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Sep 04 11:16:19 2003 +0200
+++ b/src/Pure/theory.ML	Thu Sep 04 16:04:15 2003 +0200
@@ -238,9 +238,12 @@
 fun err_in_axm name =
   error ("The error(s) above occurred in axiom " ^ quote name);
 
-fun no_vars tm =
-  if null (term_vars tm) andalso null (term_tvars tm) then tm
-  else error "Illegal schematic variable(s) in term";
+fun no_vars sg tm = (case (term_vars tm, term_tvars tm) of
+    ([], []) => tm
+  | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
+      (Pretty.str "Illegal schematic variable(s) in term:" ::
+       map (Sign.pretty_term sg) ts @
+       map (Sign.pretty_typ sg o TVar) ixns)))));
 
 fun cert_axm sg (name, raw_tm) =
   let
@@ -250,7 +253,7 @@
   in
     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
     assert (T = propT) "Term not of type prop";
-    (name, no_vars t)
+    (name, no_vars sg t)
   end;
 
 (*some duplication of code with read_def_cterm*)
@@ -266,7 +269,7 @@
 fun inferT_axm sg (name, pre_tm) =
   let
     val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);
-  in (name, no_vars t) end
+  in (name, no_vars sg t) end
   handle ERROR => err_in_axm name;