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