--- a/src/HOL/Import/import_rule.ML Sat Feb 27 16:52:30 2016 +0100
+++ b/src/HOL/Import/import_rule.ML Sat Feb 27 17:01:21 2016 +0100
@@ -425,11 +425,7 @@
| process tstate (#"l", [t1, t2]) =
gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
| process (thy, state) (#"+", [s]) =
- let
- val _ = tracing ("NOTING " ^ log_timestamp () ^ ": " ^ s)
- in
- (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
- end
+ (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
| process _ (c, _) = error ("process: unknown command: " ^ String.implode [c])
fun parse_line s =