Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 47148 7b5846065c1b
parent 46892 9920f9a75b51
child 47531 7fe7c7419489 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -172,7 +172,7 @@
   get_prover ctxt mode name params minimize_command problem
   |> minimize ctxt mode name params problem
 
-fun is_induction_fact (Untranslated_Fact ((_, (_, Induct)), _)) = true
+fun is_induction_fact (Untranslated_Fact ((_, (_, Induction)), _)) = true
   | is_induction_fact _ = false
 
 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
isabelle