# HG changeset patch
# User wenzelm
# Date 1452369360 -3600
# Node ID 092046740f17f4c9ff007c46f011e04af7e81e9e
# Parent  e2b768b0035de418fc2a712a4e2363f8aa02647e
suppress somewhat pointless description (NB: this is displayed in 'print_methods');

diff -r e2b768b0035d -r 092046740f17 src/HOL/Eisbach/method_closure.ML
--- 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;