# HG changeset patch
# User blanchet
# Date 1411055696 -7200
# Node ID 14404f6b760c85d38f10bf34addc5d876065f000
# Parent  c044539a2bdaa98679044d743b03bee5ade21454
help AFP entry 'Free-Groups' to compile

diff -r c044539a2bda -r 14404f6b760c src/HOL/Proofs/Lambda/Commutation.thy
--- a/src/HOL/Proofs/Lambda/Commutation.thy	Thu Sep 18 16:57:10 2014 +0200
+++ b/src/HOL/Proofs/Lambda/Commutation.thy	Thu Sep 18 17:54:56 2014 +0200
@@ -6,7 +6,7 @@
 header {* Abstract commutation and confluence notions *}
 
 theory Commutation
-imports Old_Datatype
+imports Main
 begin
 
 declare [[syntax_ambiguity_warning = false]]