src/Pure/Tools/find_theorems.ML
changeset 33301 1fe9fc908ec3
parent 33290 6dcb0a970783
child 33381 81269c72321a
--- a/src/Pure/Tools/find_theorems.ML	Thu Oct 29 11:26:47 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Oct 29 11:56:02 2009 +0100
@@ -18,7 +18,7 @@
     (bool * string criterion) list -> unit
 end;
 
-structure FindTheorems: FIND_THEOREMS =
+structure Find_Theorems: FIND_THEOREMS =
 struct
 
 (** search criteria **)
@@ -28,24 +28,22 @@
   Pattern of 'term;
 
 fun apply_dummies tm =
-  strip_abs tm
-  |> fst
-  |> map (Term.dummy_pattern o snd)
-  |> betapplys o pair tm
-  |> (fn x => Term.replace_dummy_patterns x 1)
-  |> fst;
+  let
+    val (xs, _) = Term.strip_abs tm;
+    val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs);
+  in #1 (Term.replace_dummy_patterns tm' 1) end;
 
 fun parse_pattern ctxt nm =
   let
-    val nm' = case Syntax.parse_term ctxt nm of Const (n, _) => n | _ => nm;
     val consts = ProofContext.consts_of ctxt;
+    val nm' =
+      (case Syntax.parse_term ctxt nm of
+        Const (c, _) => c
+      | _ => Consts.intern consts nm);
   in
-    nm'
-    |> Consts.intern consts
-    |> Consts.the_abbreviation consts
-    |> snd
-    |> apply_dummies
-    handle TYPE _ => ProofContext.read_term_pattern ctxt nm
+    (case try (Consts.the_abbreviation consts) nm' of
+      SOME (_, rhs) => apply_dummies rhs
+    | NONE => ProofContext.read_term_pattern ctxt nm)
   end;
 
 fun read_criterion _ (Name name) = Name name