# HG changeset patch
# User kleing
# Date 1117012682 -7200
# Node ID c04f972bfabeb4389106f78d83f735171680982d
# Parent  03e8a88c0b54a84f3170139e0f858dafa174e0c5
more cleanup

diff -r 03e8a88c0b54 -r c04f972bfabe src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Wed May 25 11:14:59 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Wed May 25 11:18:02 2005 +0200
@@ -60,19 +60,8 @@
     |> Library.sort thm_ord |> map #2
   end;
 
-(*speed up retrieval by checking head symbol*)
-fun index_head ctxt prop =
-  (case Term.head_of (ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) prop) of
-    Const (c, _) => ([c], [])
-  | Free (x, _) => if ProofContext.is_known ctxt x then ([], [x]) else ([], [])
-  | _ => ([], []));
-
 in
 
-fun find_matching_thms extract ctxt prop =
-  find_thms ctxt (index_head ctxt prop)
-  |> select_match extract ctxt prop;
-
 fun is_matching_thm extract ctxt prop fact =
   not (null (select_match extract ctxt prop [fact]));