# HG changeset patch
# User wenzelm
# Date 1256813762 -3600
# Node ID 1fe9fc908ec376f0280e0e2d35e2cb559031956d
# Parent  939ca97f5a1106b17cfd22b4ae904c955c8f71e4
less hermetic ML;
parse_pattern: apply Consts.intern only once (Why is this done anyway?);
modernized structure names;

diff -r 939ca97f5a11 -r 1fe9fc908ec3 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Thu Oct 29 11:26:47 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML	Thu Oct 29 11:56:02 2009 +0100
@@ -11,11 +11,10 @@
       Strict of string
     | Loose of string
     | Name of string
-
   val find_consts : Proof.context -> (bool * criterion) list -> unit
 end;
 
-structure FindConsts : FIND_CONSTS =
+structure Find_Consts : FIND_CONSTS =
 struct
 
 (* search criteria *)
@@ -162,7 +161,7 @@
 
 val _ =
   OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
-    (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+    (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
       >> (Toplevel.no_timing oo find_consts_cmd));
 
 end;
diff -r 939ca97f5a11 -r 1fe9fc908ec3 src/Pure/Tools/find_theorems.ML
--- 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
diff -r 939ca97f5a11 -r 1fe9fc908ec3 src/Tools/auto_solve.ML
--- a/src/Tools/auto_solve.ML	Thu Oct 29 11:26:47 2009 +0100
+++ b/src/Tools/auto_solve.ML	Thu Oct 29 11:56:02 2009 +0100
@@ -5,7 +5,7 @@
 existing theorem.  Duplicate lemmas can be detected in this way.
 
 The implementation is based in part on Berghofer and Haftmann's
-quickcheck.ML.  It relies critically on the FindTheorems solves
+quickcheck.ML.  It relies critically on the Find_Theorems solves
 feature.
 *)
 
@@ -45,8 +45,8 @@
   let
     val ctxt = Proof.context_of state;
 
-    val crits = [(true, FindTheorems.Solves)];
-    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
+    val crits = [(true, Find_Theorems.Solves)];
+    fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
 
     fun prt_result (goal, results) =
       let
@@ -57,7 +57,7 @@
       in
         Pretty.big_list
           (msg ^ " could be solved directly with:")
-          (map (FindTheorems.pretty_thm ctxt) results)
+          (map (Find_Theorems.pretty_thm ctxt) results)
       end;
 
     fun seek_against_goal () =