src/HOL/Eisbach/method_closure.ML

--- a/src/HOL/Eisbach/method_closure.ML	Tue Jan 12 11:00:55 2016 +1100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Jan 12 11:03:40 2016 +1100
@@ -181,11 +181,6 @@
         >> K {init = I, attribute = Named_Theorems.add full_name, pos = pos};
   in (full_name, parser) end;
 
-fun dummy_named_thm named_thm =
-  Context.proof_map
-    (Named_Theorems.clear named_thm
-      #> Named_Theorems.add_thm named_thm Drule.free_dummy_thm);
-
 fun parse_term_args args =
   Args.context :|-- (fn ctxt =>
     let