# HG changeset patch
# User wenzelm
# Date 1206827760 -3600
# Node ID 3f0231b880a7802ae9df39e91d9a5899277dfa17
# Parent  1873915c64a98fbeeb88e8f07bc2ec796ff964e9
simplified print_simpset;

diff -r 1873915c64a9 -r 3f0231b880a7 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 29 22:55:57 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 29 22:56:00 2008 +0100
@@ -466,9 +466,7 @@
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
 
 val print_simpset = Toplevel.unknown_context o
-  Toplevel.keep (Toplevel.node_case
-    (Context.cases Simplifier.print_simpset Simplifier.print_local_simpset)
-    (Simplifier.print_local_simpset o Proof.context_of));
+  Toplevel.keep (Simplifier.print_ss o Simplifier.local_simpset_of o Toplevel.context_of);
 
 val print_rules = Toplevel.unknown_context o
   Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);