src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 42793 88bee9f6eec7
parent 42697 9bc5dc48f1a5
child 42958 034fc4d0c909
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -2004,9 +2004,8 @@
     1.4    map (wf_constraint_for rel side concl) main |> foldr1 s_conj
     1.5  
     1.6  fun terminates_by ctxt timeout goal tac =
     1.7 -  can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
     1.8 -       #> SINGLE (DETERM_TIMEOUT timeout
     1.9 -                                 (tac ctxt (auto_tac (clasimpset_of ctxt))))
    1.10 +  can (SINGLE (Classical.safe_tac ctxt) #> the
    1.11 +       #> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt)))
    1.12         #> the #> Goal.finish ctxt) goal
    1.13  
    1.14  val max_cached_wfs = 50