Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
got caught once again by SML's pattern maching (ctor vs. var)
authorblanchet
Thu, 16 Sep 2010 16:54:42 +0200
changeset 39496 a52a4e4399c1
parent 39495 bb4fb9ffe2d1
child 39497 fa16349939b7
got caught once again by SML's pattern maching (ctor vs. var)
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 16 16:24:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 16 16:54:42 2010 +0200
@@ -20,6 +20,7 @@
 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
 struct
 
+open ATP_Proof
 open Sledgehammer_Util
 open Sledgehammer_Filter
 open Sledgehammer_Translate
@@ -28,9 +29,9 @@
 
 (* wrapper for calling external prover *)
 
-fun string_for_failure ATP_Proof.Unprovable = "Unprovable."
-  | string_for_failure ATP_Proof.TimedOut = "Timed out."
-  | string_for_failure ATP_Proof.Interrupted = "Interrupted."
+fun string_for_failure Unprovable = "Unprovable."
+  | string_for_failure TimedOut = "Timed out."
+  | string_for_failure Interrupted = "Interrupted."
   | string_for_failure _ = "Unknown error."
 
 fun n_theorems names =
isabelle