# HG changeset patch
# User urbanc
# Date 1162393891 -3600
# Node ID afdd72fc6c4fa82984b8b4831412ac60e4fc9ba0
# Parent  8a1d62375ff853b3e7e2cae68cc5b5d1842fe4fb
changed to use Lam_Funs

diff -r 8a1d62375ff8 -r afdd72fc6c4f src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Wed Nov 01 15:51:11 2006 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Wed Nov 01 16:11:31 2006 +0100
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory CR
-imports Lam_substs
+imports Lam_Funs
 begin
 
 text {* The Church-Rosser proof from Barendregt's book *}