# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID 34d0ac1bdac6cfb78691e82276ad1813fdb7a6b4
# Parent  ef811090e1062cd1c381c19b772c5f0d1a8a08d0
moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong

diff -r ef811090e106 -r 34d0ac1bdac6 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/FunDef.thy	Wed Oct 31 11:23:21 2012 +0100
@@ -5,13 +5,10 @@
 header {* Function Definitions and Termination Proofs *}
 
 theory FunDef
-imports Partial_Function Wellfounded
+imports Partial_Function SAT Wellfounded
 keywords "function" "termination" :: thy_goal and "fun" :: thy_decl
 begin
 
-ML_file "Tools/prop_logic.ML"
-ML_file "Tools/sat_solver.ML"
-
 subsection {* Definitions with default value. *}
 
 definition
diff -r ef811090e106 -r 34d0ac1bdac6 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Nitpick.thy	Wed Oct 31 11:23:21 2012 +0100
@@ -8,7 +8,7 @@
 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
 
 theory Nitpick
-imports Map Quotient SAT Record
+imports Hilbert_Choice List Map Quotient Record Sledgehammer
 keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
 begin
 
diff -r ef811090e106 -r 34d0ac1bdac6 src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/SAT.thy	Wed Oct 31 11:23:21 2012 +0100
@@ -2,15 +2,17 @@
     Author:     Alwen Tiu, Tjark Weber
     Copyright   2005
 
-Basic setup for the 'sat' and 'satx' tactic.
+Basic setup for the 'sat' and 'satx' tactics.
 *)
 
 header {* Reconstructing external resolution proofs for propositional logic *}
 
 theory SAT
-imports Hilbert_Choice List Sledgehammer
+imports HOL
 begin
 
+ML_file "Tools/prop_logic.ML"
+ML_file "Tools/sat_solver.ML"
 ML_file "Tools/sat_funcs.ML"
 
 ML {* structure sat = SATFunc(cnf) *}