src/HOL/HOLCF/Tools/fixrec.ML
changeset 57945 cacb00a569e0
parent 51717 9e7d1c139569
child 57954 c52223cd1003
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Fri Aug 15 18:02:34 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Aug 16 11:35:33 2014 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4            "or simp rules are configured for all non-HOLCF constants.\n" ^
     1.5            "The error occurred for the goal statement:\n" ^
     1.6            Syntax.string_of_term lthy prop)
     1.7 -        val rules = Cont2ContData.get lthy
     1.8 +        val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
     1.9          val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules))
    1.10          val slow_tac = SOLVED' (simp_tac lthy)
    1.11          val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err