--- a/src/Pure/Tools/print_operation.ML Tue Jul 22 13:36:51 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML Tue Jul 22 14:03:00 2014 +0200
@@ -64,7 +64,8 @@
register "context" "context of local theory target" Toplevel.pretty_context;
val _ =
- register "cases" "cases of proof context" (Proof_Context.pretty_cases o Toplevel.context_of);
+ register "cases" "cases of proof context"
+ (Proof_Context.pretty_cases o Toplevel.context_of);
val _ =
register "terms" "term bindings of proof context"
@@ -72,7 +73,7 @@
val _ =
register "theorems" "theorems of local theory or proof context"
- (single o Isar_Cmd.pretty_theorems false);
+ (Isar_Cmd.pretty_theorems false);
val _ =
register "state" "proof state" Toplevel.pretty_state;