# HG changeset patch
# User wenzelm
# Date 965321115 -7200
# Node ID e6dfc9c9bf89bb50457d0e40a3a555e18279ce74
# Parent  8cd9cfc22dd71f7b5ef5a8cdaa410f1d54eeef69
added setmp_verbose;

diff -r 8cd9cfc22dd7 -r e6dfc9c9bf89 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Aug 03 18:44:55 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 03 18:45:15 2000 +0200
@@ -17,6 +17,7 @@
   val show_hyps: bool ref
   val pretty_thm: thm -> Pretty.T
   val verbose: bool ref
+  val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_binds: context -> unit
   val print_thms: context -> unit
   val print_cases: context -> unit
@@ -151,6 +152,8 @@
 fun verb f x = if ! verbose then f (x ()) else [];
 fun verb_single x = verb Library.single x;
 
+fun setmp_verbose f x = Library.setmp verbose true f x;
+
 fun pretty_items prt name items =
   let
     fun prt_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x]
@@ -232,8 +235,9 @@
     fun prt_fix (x, x') = Pretty.block
       [prt_term (Syntax.free x), Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
 
-    fun prt_fixes xs = Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
-      Pretty.commas (map prt_fix xs));
+    fun prt_fixes [] = []
+      | prt_fixes xs = [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
+          Pretty.commas (map prt_fix xs))];
 
     (*defaults*)
     fun prt_atom prt prtT (x, X) = Pretty.block
@@ -249,7 +253,7 @@
     val prt_defS = prt_atom prt_varT prt_sort;
   in
     verb_single (K pretty_thy) @
-    (if null fixes then [] else [prt_fixes (rev fixes)]) @
+    prt_fixes (rev (filter_out (can Syntax.dest_internal o #1) fixes)) @
     pretty_prems ctxt @
     verb pretty_binds (K ctxt) @
     verb pretty_thms (K ctxt) @