src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 42793 88bee9f6eec7
parent 42415 10accf397ab6
child 45479 3387d482e0a9
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -1050,8 +1050,7 @@
     1.4                   ()
     1.5          val goal = prop |> cterm_of thy |> Goal.init
     1.6        in
     1.7 -        (goal |> SINGLE (DETERM_TIMEOUT auto_timeout
     1.8 -                                        (auto_tac (clasimpset_of ctxt)))
     1.9 +        (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
    1.10                |> the |> Goal.finish ctxt; true)
    1.11          handle THM _ => false
    1.12               | TimeLimit.TimeOut => false