--- 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
--- 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)
--- 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