# HG changeset patch
# User bulwahn
# Date 1291629165 -3600
# Node ID 29e5cae935842962bb81a9a71de3e72ab1672835
# Parent  890fefa597af2bfd9ed90d3e645d91c34b03bf9a
commenting out sledgehammer_mtd in Mutabelle

diff -r 890fefa597af -r 29e5cae93584 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 10:52:45 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 10:52:45 2010 +0100
@@ -24,9 +24,9 @@
 
 val solve_direct_mtd : mtd
 val try_mtd : mtd
-
+(*
 val sledgehammer_mtd : mtd
-
+*)
 (*
 val refute_mtd : mtd
 val nitpick_mtd : mtd
@@ -156,7 +156,7 @@
 val try_mtd = ("try", invoke_try)
 
 (** sledgehammer **)
-
+(*
 fun invoke_sledgehammer thy t =
   if can (Goal.prove_global thy (Term.add_free_names t [])  [] t)
       (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
@@ -165,7 +165,7 @@
     (Unsolved, ([], NONE))
 
 val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
-
+*)
 (*
 fun invoke_refute thy t =
   let