remove unused code

--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Tue Jan 12 11:00:55 2016 +1100
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Tue Jan 12 11:03:40 2016 +1100
@@ -76,35 +76,9 @@
     |> restore_tags thm
   end;
 
-(* FIXME unused *)
-fun read_instantiate_no_thm ctxt insts fixes =
-  let
-    val (type_insts, term_insts) =
-      List.partition (fn (((x, _) : indexname), _) => String.isPrefix "'" x) insts;
-
-    val ctxt1 =
-      ctxt
-      |> Context_Position.not_really
-      |> Proof_Context.add_fixes_cmd fixes |> #2;
-
-    val typs =
-      map snd type_insts
-      |> Syntax.read_typs ctxt1;
-
-    val typ_insts' = map2 (fn (xi, _) => fn T => (xi, T)) type_insts typs;
-
-    val terms =
-      map snd term_insts
-      |> Syntax.read_terms ctxt1;
-
-    val term_insts' = map2 (fn (xi, _) => fn t => (xi, t)) term_insts terms;
-
-  in (typ_insts', term_insts') end;
-
 
 datatype rule_inst =
   Named_Insts of ((indexname * string) * (term -> unit)) list * (binding * string option * mixfix) list
-(*| Unchecked_Of_Insts of (string option list * string option list) * (binding * string option * mixfix) list*)
 | Term_Insts of (indexname * term) list
 | Unchecked_Term_Insts of term option list * term option list;
 

--- a/src/HOL/Eisbach/match_method.ML	Tue Jan 12 11:00:55 2016 +1100
+++ b/src/HOL/Eisbach/match_method.ML	Tue Jan 12 11:03:40 2016 +1100
@@ -434,8 +434,6 @@
       |> add_focus_schematics (snd schematics)
       |> fold_map add_focus_prem (rev prems)
 
-    val local_prems = map2 pair prem_ids (rev prems);
-
   in
     (prem_ids,
       {context = ctxt',

--- 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