src/HOL/Tools/simpdata.ML
changeset 32177 bc02c5bfcb5b
parent 32155 e2bf2f73b0c8
child 33339 d41f77196338
     1.1 --- a/src/HOL/Tools/simpdata.ML	Fri Jul 24 21:21:45 2009 +0200
     1.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Jul 24 21:34:37 2009 +0200
     1.3 @@ -126,27 +126,25 @@
     1.4  
     1.5  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
     1.6  
     1.7 -structure SplitterData =
     1.8 -struct
     1.9 -  structure Simplifier = Simplifier
    1.10 -  val mk_eq           = mk_eq
    1.11 -  val meta_eq_to_iff  = @{thm meta_eq_to_obj_eq}
    1.12 -  val iffD            = @{thm iffD2}
    1.13 -  val disjE           = @{thm disjE}
    1.14 -  val conjE           = @{thm conjE}
    1.15 -  val exE             = @{thm exE}
    1.16 -  val contrapos       = @{thm contrapos_nn}
    1.17 -  val contrapos2      = @{thm contrapos_pp}
    1.18 -  val notnotD         = @{thm notnotD}
    1.19 -end;
    1.20 +structure Splitter = Splitter
    1.21 +(
    1.22 +  val thy = @{theory}
    1.23 +  val mk_eq = mk_eq
    1.24 +  val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
    1.25 +  val iffD = @{thm iffD2}
    1.26 +  val disjE = @{thm disjE}
    1.27 +  val conjE = @{thm conjE}
    1.28 +  val exE = @{thm exE}
    1.29 +  val contrapos = @{thm contrapos_nn}
    1.30 +  val contrapos2 = @{thm contrapos_pp}
    1.31 +  val notnotD = @{thm notnotD}
    1.32 +);
    1.33  
    1.34 -structure Splitter = SplitterFun(SplitterData);
    1.35 -
    1.36 -val split_tac        = Splitter.split_tac;
    1.37 +val split_tac = Splitter.split_tac;
    1.38  val split_inside_tac = Splitter.split_inside_tac;
    1.39  
    1.40 -val op addsplits     = Splitter.addsplits;
    1.41 -val op delsplits     = Splitter.delsplits;
    1.42 +val op addsplits = Splitter.addsplits;
    1.43 +val op delsplits = Splitter.delsplits;
    1.44  
    1.45  
    1.46  (* integration of simplifier with classical reasoner *)