--- 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:"
--- 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);