--- a/src/HOL/Eisbach/method_closure.ML Sat Jan 09 13:31:31 2016 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Sat Jan 09 20:56:00 2016 +0100
@@ -272,8 +272,7 @@
|> Proof_Context.restore_naming lthy
|> put_closure name
{vars = term_args', named_thms = named_thms, methods = method_args, body = text'}
- |> Method.local_setup name (parser term_args' (recursive_method term_args' text'))
- "(defined in Eisbach)"
+ |> Method.local_setup name (parser term_args' (recursive_method term_args' text')) ""
|> pair (Local_Theory.full_name lthy name)
end;