# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID e1172791ad0d95400c81d42f972029962d1eb47d
# Parent  3e060b1c844b0d966855bb013ed41549baa4cab4
compile

diff -r 3e060b1c844b -r e1172791ad0d src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri May 27 10:30:08 2011 +0200
@@ -24,7 +24,7 @@
 val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
 
 val solve_direct_mtd : mtd
-val try_mtd : mtd
+val try_methods_mtd : mtd
 (*
 val sledgehammer_mtd : mtd
 *)
@@ -141,7 +141,7 @@
   let
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) 
   in
-    case Solve_Direct.solve_direct false state of
+    case Solve_Direct.solve_direct state of
       (true, _) => (Solved, [])
     | (false, _) => (Unsolved, [])
   end
@@ -150,16 +150,16 @@
 
 (** try **)
 
-fun invoke_try thy t =
+fun invoke_try_methods thy t =
   let
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
   in
-    case Try.invoke_try (SOME (seconds 5.0)) ([], [], [], []) state of
+    case Try_Methods.try_methods (SOME (seconds 5.0)) ([], [], [], []) state of
       true => (Solved, [])
     | false => (Unsolved, [])
   end
 
-val try_mtd = ("try", invoke_try)
+val try_methods_mtd = ("try_methods", invoke_try_methods)
 
 (** sledgehammer **)
 (*
@@ -199,7 +199,7 @@
     val ctxt = Proof_Context.init_global thy
     val state = Proof.init ctxt
     val (res, _) = Nitpick.pick_nits_in_term state
-      (Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t
+      (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] t
     val _ = Output.urgent_message ("Nitpick: " ^ res)
   in
     (rpair []) (case res of