src/HOL/List.thy
changeset 42361 23f352990944
parent 42359 6ca5407863ed
child 42411 ff997038e8eb
     1.1 --- a/src/HOL/List.thy	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -395,8 +395,8 @@
     1.4  
     1.5    fun abs_tr ctxt (p as Free (s, T)) e opti =
     1.6          let
     1.7 -          val thy = ProofContext.theory_of ctxt;
     1.8 -          val s' = ProofContext.intern_const ctxt s;
     1.9 +          val thy = Proof_Context.theory_of ctxt;
    1.10 +          val s' = Proof_Context.intern_const ctxt s;
    1.11          in
    1.12            if Sign.declared_const thy s'
    1.13            then (pat_tr ctxt p e opti, false)