# HG changeset patch
# User wenzelm
# Date 1236510972 -3600
# Node ID 77c3f2135a0f6e3dc29143dc41b2f180344313ad
# Parent  36d0e00af606c3b95c8485d5bacf24fb3ee4db2f
proper context for Simplifier.pretty_ss;

diff -r 36d0e00af606 -r 77c3f2135a0f src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Mar 08 12:15:58 2009 +0100
+++ b/src/Pure/Isar/code.ML	Sun Mar 08 12:16:12 2009 +0100
@@ -416,12 +416,12 @@
       Pretty.block [
         Pretty.str "preprocessing simpset:",
         Pretty.fbrk,
-        Simplifier.pretty_ss pre
+        Simplifier.pretty_ss ctxt pre
       ],
       Pretty.block [
         Pretty.str "postprocessing simpset:",
         Pretty.fbrk,
-        Simplifier.pretty_ss post
+        Simplifier.pretty_ss ctxt post
       ],
       Pretty.block (
         Pretty.str "function transformers:"
diff -r 36d0e00af606 -r 77c3f2135a0f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 08 12:15:58 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 08 12:16:12 2009 +0100
@@ -359,7 +359,9 @@
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
 
 val print_simpset = Toplevel.unknown_context o
-  Toplevel.keep (Pretty.writeln o Simplifier.pretty_ss o Simplifier.local_simpset_of o Toplevel.context_of);
+  Toplevel.keep (fn state =>
+    let val ctxt = Toplevel.context_of state
+    in Pretty.writeln (Simplifier.pretty_ss ctxt (Simplifier.local_simpset_of ctxt)) end);
 
 val print_rules = Toplevel.unknown_context o
   Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);