# 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 () =