src/HOL/HOLCF/Tools/fixrec.ML
changeset 42361 23f352990944
parent 42151 4da4fc77664b
child 43324 2b47822868e4
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4    (spec : (Attrib.binding * term) list)
     1.5    (lthy : local_theory) =
     1.6    let
     1.7 -    val thy = ProofContext.theory_of lthy
     1.8 +    val thy = Proof_Context.theory_of lthy
     1.9      val names = map (Binding.name_of o fst o fst) fixes
    1.10      val all_names = space_implode "_" names
    1.11      val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec)
    1.12 @@ -355,7 +355,7 @@
    1.13          (all_names ~~ (spec ~~ skips))
    1.14      val blocks = map block_of_name names
    1.15  
    1.16 -    val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy)
    1.17 +    val matcher_tab = FixrecMatchData.get (Proof_Context.theory_of lthy)
    1.18      fun match_name c =
    1.19        case Symtab.lookup matcher_tab c of SOME m => m
    1.20          | NONE => fixrec_err ("unknown pattern constructor: " ^ c)