--- a/src/HOL/List.thy Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/List.thy Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/List.thy
- ID: $Id$
Author: Tobias Nipkow
*)
@@ -359,7 +358,7 @@
fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
let
- val x = Free (Name.variant (add_term_free_names (p$e, [])) "x", dummyT);
+ val x = Free (Name.variant (OldTerm.add_term_free_names (p$e, [])) "x", dummyT);
val e = if opti then singl e else e;
val case1 = Syntax.const "_case1" $ p $ e;
val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN