equal
deleted
inserted
replaced
121 end |
121 end |
122 |
122 |
123 val _ = |
123 val _ = |
124 Outer_Syntax.improper_command @{command_spec "find_unused_assms"} |
124 Outer_Syntax.improper_command @{command_spec "find_unused_assms"} |
125 "find theorems with (potentially) superfluous assumptions" |
125 "find theorems with (potentially) superfluous assumptions" |
126 (Scan.option Parse.name |
126 (Scan.option Parse.name >> (fn name => |
127 >> (fn opt_thy_name => |
127 Toplevel.keep (fn state => print_unused_assms (Toplevel.context_of state) name))) |
128 Toplevel.no_timing o Toplevel.keep (fn state => |
|
129 print_unused_assms (Toplevel.context_of state) opt_thy_name))) |
|
130 |
128 |
131 end |
129 end |