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 46340 cac402c486b0
parent 46320 0b8b73b49848
child 46409 d4754183ccce 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 26 20:49:54 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 26 20:49:54 2012 +0100
@@ -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 ((_, Induction), _)) = true
+fun is_induction_fact (Untranslated_Fact ((_, (_, Induct)), _)) = true
   | is_induction_fact _ = false
 
 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
isabelle