src/Pure/Isar/find_theorems.ML
changeset 16486 1a12cdb6ee6b
parent 16088 f084ba24de29
child 16895 df67fc190e06
--- a/src/Pure/Isar/find_theorems.ML	Mon Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Mon Jun 20 22:13:59 2005 +0200
@@ -38,7 +38,7 @@
   | read_criterion _ Intro = Intro
   | read_criterion _ Elim = Elim
   | read_criterion _ Dest = Dest
-  | read_criterion ctxt (Simp str) = 
+  | read_criterion ctxt (Simp str) =
       Simp (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]))
   | read_criterion ctxt (Pattern str) =
       Pattern (hd (ProofContext.read_term_pats TypeInfer.logicT ctxt [str]));
@@ -70,15 +70,15 @@
     val sg = ProofContext.sign_of ctxt;
     val tsig = Sign.tsig_of sg;
 
-    val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;    
+    val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg;
 
-    fun matches pat = 
-      is_nontrivial pat andalso 
+    fun matches pat =
+      is_nontrivial pat andalso
       Pattern.matches tsig (if po then (pat,obj) else (obj,pat))
       handle Pattern.MATCH => false;
 
     val match_thm = matches o extract_term o Thm.prop_of
-  in       
+  in
     List.exists match_thm (extract_thms thm)
   end;
 
@@ -93,7 +93,7 @@
 
 (*filter that just looks for a string in the name,
   substring match only (no regexps are performed)*)
-fun filter_name str_pat ((name, _), _) = is_substring str_pat name;
+fun filter_name str_pat (thmref, _) = is_substring str_pat (PureThy.name_of_thmref thmref);
 
 
 (* filter intro/elim/dest rules *)
@@ -121,8 +121,8 @@
       hd o Logic.strip_imp_prems);
     val prems = Logic.prems_of_goal goal 1;
   in
-    prems |> 
-    List.exists (fn prem => 
+    prems |>
+    List.exists (fn prem =>
       is_matching_thm extract_elim ctxt true prem thm
       andalso (check_thm ctxt) thm)
   end;