--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Tue Apr 09 13:55:28 2013 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Tue Apr 09 15:29:25 2013 +0200
@@ -123,9 +123,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
"find theorems with (potentially) superfluous assumptions"
- (Scan.option Parse.name
- >> (fn opt_thy_name =>
- Toplevel.no_timing o Toplevel.keep (fn state =>
- print_unused_assms (Toplevel.context_of state) opt_thy_name)))
+ (Scan.option Parse.name >> (fn name =>
+ Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name)))
end