# HG changeset patch
# User wenzelm
# Date 934230169 -7200
# Node ID c9b03d9d664783c3849ee56821bc43b4dde92272
# Parent  7fede88e5c73414fb0ebb9928a1c2bc9c5d00744
tuned strings_of_context;
fix: check identifier;

diff -r 7fede88e5c73 -r c9b03d9d6647 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Aug 09 22:22:01 1999 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Aug 09 22:22:49 1999 +0200
@@ -170,7 +170,9 @@
     val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
 
     (*fixes*)
-    fun prt_fix (x, x') = Pretty.str (x ^ " = " ^ x');
+    fun prt_fixes xs = Pretty.block (Pretty.str "Fixed variables:" :: Pretty.brk 1 ::
+      Pretty.commas (map (fn (x, x') => Pretty.str (x ^ " = " ^ x')) xs));
+
 
     (* defaults *)
 
@@ -188,7 +190,7 @@
   in
     verb_string pretty_thy @
     (if null fixes andalso not (! verbose) then []
-     else [Pretty.string_of (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)))]) @
+      else [Pretty.string_of (prt_fixes (rev fixes))]) @
     strings_of_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" prems @
     verb strings_of_binds ctxt @
     verb strings_of_thms ctxt @
@@ -353,7 +355,10 @@
 fun get_skolem (Context {asms = (_, (fixes, _)), ...}) x = assoc (fixes, x);
 
 fun check_skolem ctxt check x =
-  if check andalso can Syntax.dest_skolem x then
+  if not check then x
+  else if not (Syntax.is_identifier x) then
+    raise CONTEXT ("Bad variable name: " ^ quote x, ctxt)
+  else if can Syntax.dest_skolem x then
     raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt)
   else x;