1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
     1.5  
     1.6  val solve_direct_mtd : mtd
     1.7 -val try_mtd : mtd
     1.8 +val try_methods_mtd : mtd
     1.9  (*
    1.10  val sledgehammer_mtd : mtd
    1.11  *)
    1.12 @@ -141,7 +141,7 @@
    1.13    let
    1.14      val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) 
    1.15    in
    1.16 -    case Solve_Direct.solve_direct false state of
    1.17 +    case Solve_Direct.solve_direct state of
    1.18        (true, _) => (Solved, [])
    1.19      | (false, _) => (Unsolved, [])
    1.20    end
    1.21 @@ -150,16 +150,16 @@
    1.22  
    1.23  (** try **)
    1.24  
    1.25 -fun invoke_try thy t =
    1.26 +fun invoke_try_methods thy t =
    1.27    let
    1.28      val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
    1.29    in
    1.30 -    case Try.invoke_try (SOME (seconds 5.0)) ([], [], [], []) state of
    1.31 +    case Try_Methods.try_methods (SOME (seconds 5.0)) ([], [], [], []) state of
    1.32        true => (Solved, [])
    1.33      | false => (Unsolved, [])
    1.34    end
    1.35  
    1.36 -val try_mtd = ("try", invoke_try)
    1.37 +val try_methods_mtd = ("try_methods", invoke_try_methods)
    1.38  
    1.39  (** sledgehammer **)
    1.40  (*
    1.41 @@ -199,7 +199,7 @@
    1.42      val ctxt = Proof_Context.init_global thy
    1.43      val state = Proof.init ctxt
    1.44      val (res, _) = Nitpick.pick_nits_in_term state
    1.45 -      (Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t
    1.46 +      (Nitpick_Isar.default_params thy []) Nitpick.Normal 1 1 1 [] [] t
    1.47      val _ = Output.urgent_message ("Nitpick: " ^ res)
    1.48    in
    1.49      (rpair []) (case res of