# HG changeset patch
# User haftmann
# Date 1164187211 -3600
# Node ID 03ca07d478be74d97cf46202cb1568f0c016f859
# Parent  f825e0b4d566a15e9b13bba95bb9f14528dd171d
removed Extraction dependency

diff -r f825e0b4d566 -r 03ca07d478be src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Wed Nov 22 10:20:09 2006 +0100
+++ b/src/HOL/ATP_Linkup.thy	Wed Nov 22 10:20:11 2006 +0100
@@ -7,7 +7,7 @@
 header{* The Isabelle-ATP Linkup *}
 
 theory ATP_Linkup
-imports Hilbert_Choice Map Extraction
+imports Map Hilbert_Choice
 uses
   "Tools/polyhash.ML"
   "Tools/ATP/AtpCommunication.ML"