# HG changeset patch
# User blanchet
# Date 1402585323 -7200
# Node ID 25aff3b8d550098c4c867a64b9b18e4980e1f0f7
# Parent  7fca4159117f4ca5155352de89c2518a18778eb8
tuned dependencies

diff -r 7fca4159117f -r 25aff3b8d550 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Nitpick.thy	Thu Jun 12 17:02:03 2014 +0200
@@ -8,7 +8,7 @@
 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
 
 theory Nitpick
-imports BNF_FP_Base Map Record
+imports Record
 keywords
   "nitpick" :: diag and
   "nitpick_params" :: thy_decl
diff -r 7fca4159117f -r 25aff3b8d550 src/HOL/Random.thy
--- a/src/HOL/Random.thy	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Random.thy	Thu Jun 12 17:02:03 2014 +0200
@@ -4,7 +4,7 @@
 header {* A HOL random engine *}
 
 theory Random
-imports Code_Numeral List
+imports List
 begin
 
 notation fcomp (infixl "\<circ>>" 60)
diff -r 7fca4159117f -r 25aff3b8d550 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Jun 12 17:02:03 2014 +0200
@@ -7,7 +7,7 @@
 header {* Sledgehammer: Isabelle--ATP Linkup *}
 
 theory Sledgehammer
-imports Presburger ATP SMT2
+imports Presburger SMT2
 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
 begin