src/HOL/HOLCF/Tools/fixrec.ML
changeset 58957 c9e744ea8a38
parent 57954 c52223cd1003
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4            "The error occurred for the goal statement:\n" ^
     1.5            Syntax.string_of_term lthy prop)
     1.6          val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
     1.7 -        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)))
     1.8 +        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac lthy (rev rules)))
     1.9          val slow_tac = SOLVED' (simp_tac lthy)
    1.10          val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
    1.11        in