src/HOL/List.thy
changeset 42359 6ca5407863ed
parent 42264 b6c1b0c4c511
child 42361 23f352990944
     1.1 --- a/src/HOL/List.thy	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -396,7 +396,7 @@
     1.4    fun abs_tr ctxt (p as Free (s, T)) e opti =
     1.5          let
     1.6            val thy = ProofContext.theory_of ctxt;
     1.7 -          val s' = Sign.intern_const thy s;
     1.8 +          val s' = ProofContext.intern_const ctxt s;
     1.9          in
    1.10            if Sign.declared_const thy s'
    1.11            then (pat_tr ctxt p e opti, false)