1.1 --- a/src/Pure/Isar/code.ML	Sun Mar 08 12:15:58 2009 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Sun Mar 08 12:16:12 2009 +0100
     1.3 @@ -416,12 +416,12 @@
     1.4        Pretty.block [
     1.5          Pretty.str "preprocessing simpset:",
     1.6          Pretty.fbrk,
     1.7 -        Simplifier.pretty_ss pre
     1.8 +        Simplifier.pretty_ss ctxt pre
     1.9        ],
    1.10        Pretty.block [
    1.11          Pretty.str "postprocessing simpset:",
    1.12          Pretty.fbrk,
    1.13 -        Simplifier.pretty_ss post
    1.14 +        Simplifier.pretty_ss ctxt post
    1.15        ],
    1.16        Pretty.block (
    1.17          Pretty.str "function transformers:"

     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 08 12:15:58 2009 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 08 12:16:12 2009 +0100
     2.3 @@ -359,7 +359,9 @@
     2.4    Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
     2.5  
     2.6  val print_simpset = Toplevel.unknown_context o
     2.7 -  Toplevel.keep (Pretty.writeln o Simplifier.pretty_ss o Simplifier.local_simpset_of o Toplevel.context_of);
     2.8 +  Toplevel.keep (fn state =>
     2.9 +    let val ctxt = Toplevel.context_of state
    2.10 +    in Pretty.writeln (Simplifier.pretty_ss ctxt (Simplifier.local_simpset_of ctxt)) end);
    2.11  
    2.12  val print_rules = Toplevel.unknown_context o
    2.13    Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);