renamed functor SplitterFun to Splitter, require explicit theory;

--- a/src/FOL/simpdata.ML	Fri Jul 24 21:21:45 2009 +0200
+++ b/src/FOL/simpdata.ML	Fri Jul 24 21:34:37 2009 +0200
@@ -95,27 +95,25 @@
 
 (*** Case splitting ***)
 
-structure SplitterData =
-  struct
-  structure Simplifier = Simplifier
-  val mk_eq          = mk_eq
+structure Splitter = Splitter
+(
+  val thy = @{theory}
+  val mk_eq = mk_eq
   val meta_eq_to_iff = @{thm meta_eq_to_iff}
-  val iffD           = @{thm iffD2}
-  val disjE          = @{thm disjE}
-  val conjE          = @{thm conjE}
-  val exE            = @{thm exE}
-  val contrapos      = @{thm contrapos}
-  val contrapos2     = @{thm contrapos2}
-  val notnotD        = @{thm notnotD}
-  end;
+  val iffD = @{thm iffD2}
+  val disjE = @{thm disjE}
+  val conjE = @{thm conjE}
+  val exE = @{thm exE}
+  val contrapos = @{thm contrapos}
+  val contrapos2 = @{thm contrapos2}
+  val notnotD = @{thm notnotD}
+);
 
-structure Splitter = SplitterFun(SplitterData);
-
-val split_tac        = Splitter.split_tac;
+val split_tac = Splitter.split_tac;
 val split_inside_tac = Splitter.split_inside_tac;
-val split_asm_tac    = Splitter.split_asm_tac;
-val op addsplits     = Splitter.addsplits;
-val op delsplits     = Splitter.delsplits;
+val split_asm_tac = Splitter.split_asm_tac;
+val op addsplits = Splitter.addsplits;
+val op delsplits = Splitter.delsplits;
 
 
 (*** Standard simpsets ***)

--- a/src/HOL/Tools/simpdata.ML	Fri Jul 24 21:21:45 2009 +0200
+++ b/src/HOL/Tools/simpdata.ML	Fri Jul 24 21:34:37 2009 +0200
@@ -126,27 +126,25 @@
 
 val safe_solver = mk_solver "HOL safe" safe_solver_tac;
 
-structure SplitterData =
-struct
-  structure Simplifier = Simplifier
-  val mk_eq           = mk_eq
-  val meta_eq_to_iff  = @{thm meta_eq_to_obj_eq}
-  val iffD            = @{thm iffD2}
-  val disjE           = @{thm disjE}
-  val conjE           = @{thm conjE}
-  val exE             = @{thm exE}
-  val contrapos       = @{thm contrapos_nn}
-  val contrapos2      = @{thm contrapos_pp}
-  val notnotD         = @{thm notnotD}
-end;
+structure Splitter = Splitter
+(
+  val thy = @{theory}
+  val mk_eq = mk_eq
+  val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
+  val iffD = @{thm iffD2}
+  val disjE = @{thm disjE}
+  val conjE = @{thm conjE}
+  val exE = @{thm exE}
+  val contrapos = @{thm contrapos_nn}
+  val contrapos2 = @{thm contrapos_pp}
+  val notnotD = @{thm notnotD}
+);
 
-structure Splitter = SplitterFun(SplitterData);
-
-val split_tac        = Splitter.split_tac;
+val split_tac = Splitter.split_tac;
 val split_inside_tac = Splitter.split_inside_tac;
 
-val op addsplits     = Splitter.addsplits;
-val op delsplits     = Splitter.delsplits;
+val op addsplits = Splitter.addsplits;
+val op delsplits = Splitter.delsplits;
 
 
 (* integration of simplifier with classical reasoner *)

--- a/src/Provers/splitter.ML	Fri Jul 24 21:21:45 2009 +0200
+++ b/src/Provers/splitter.ML	Fri Jul 24 21:34:37 2009 +0200
@@ -11,6 +11,7 @@
 
 signature SPLITTER_DATA =
 sig
+  val thy           : theory
   val mk_eq         : thm -> thm
   val meta_eq_to_iff: thm (* "x == y ==> x = y"                      *)
   val iffD          : thm (* "[| P = Q; Q |] ==> P"                  *)
@@ -40,18 +41,18 @@
   val setup: theory -> theory
 end;
 
-functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
+functor Splitter(Data: SPLITTER_DATA): SPLITTER =
 struct
 
 val Const (const_not, _) $ _ =
-  ObjectLogic.drop_judgment (OldGoals.the_context ())
+  ObjectLogic.drop_judgment Data.thy
     (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
 
 val Const (const_or , _) $ _ $ _ =
-  ObjectLogic.drop_judgment (OldGoals.the_context ())
+  ObjectLogic.drop_judgment Data.thy
     (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
 
-val const_Trueprop = ObjectLogic.judgment_name (OldGoals.the_context ());
+val const_Trueprop = ObjectLogic.judgment_name Data.thy;
 
 
 fun split_format_err () = error "Wrong format for split rule";