src/HOL/List.thy

--- a/src/HOL/List.thy	Sat Apr 16 13:48:45 2011 +0200
+++ b/src/HOL/List.thy	Sat Apr 16 15:25:25 2011 +0200
@@ -396,7 +396,7 @@
   fun abs_tr ctxt (p as Free (s, T)) e opti =
         let
           val thy = ProofContext.theory_of ctxt;
-          val s' = Sign.intern_const thy s;
+          val s' = ProofContext.intern_const ctxt s;
         in
           if Sign.declared_const thy s'
           then (pat_tr ctxt p e opti, false)