# HG changeset patch
# User blanchet
# Date 1402527649 -7200
# Node ID dca8d06ecbbaa6096ab5041126dc7777f11114b8
# Parent  ec5ff6bb2a92440cd932e5ac75ddda31d77b7fa3
reduces Sledgehammer dependencies

diff -r ec5ff6bb2a92 -r dca8d06ecbba src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/List.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
+imports Sledgehammer Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
 begin
 
 datatype_new (set: 'a) list =
diff -r ec5ff6bb2a92 -r dca8d06ecbba src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Nitpick.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -8,7 +8,7 @@
 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
 
 theory Nitpick
-imports BNF_FP_Base Map Record Sledgehammer
+imports BNF_FP_Base Map Record
 keywords
   "nitpick" :: diag and
   "nitpick_params" :: thy_decl
diff -r ec5ff6bb2a92 -r dca8d06ecbba src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -5,7 +5,7 @@
 header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
 
 theory SMT
-imports ATP
+imports Record
 keywords "smt_status" :: diag
 begin
 
diff -r ec5ff6bb2a92 -r dca8d06ecbba src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Jun 12 01:00:49 2014 +0200
@@ -7,7 +7,7 @@
 header {* Sledgehammer: Isabelle--ATP Linkup *}
 
 theory Sledgehammer
-imports ATP SMT2
+imports Presburger ATP SMT2
 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
 begin