src/Pure/simplifier.ML
changeset 22846 fb79144af9a3
parent 22770 615e19792c92
child 23086 12320f6e2523
     1.1 --- a/src/Pure/simplifier.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -97,19 +97,16 @@
     1.4  (* global simpsets *)
     1.5  
     1.6  structure GlobalSimpset = TheoryDataFun
     1.7 -(struct
     1.8 -  val name = "Pure/simpset";
     1.9 +(
    1.10    type T = simpset ref;
    1.11 -
    1.12    val empty = ref empty_ss;
    1.13 -  fun copy (ref ss) = ref ss: T;            (*create new reference!*)
    1.14 +  fun copy (ref ss) = ref ss: T;
    1.15    fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
    1.16    fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
    1.17 -  fun print _ (ref ss) = print_ss ss;
    1.18 -end);
    1.19 +);
    1.20  
    1.21  val _ = Context.add_setup GlobalSimpset.init;
    1.22 -val print_simpset = GlobalSimpset.print;
    1.23 +fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
    1.24  val get_simpset = ! o GlobalSimpset.get;
    1.25  
    1.26  val change_simpset_of = change o GlobalSimpset.get;
    1.27 @@ -133,15 +130,12 @@
    1.28  (* local simpsets *)
    1.29  
    1.30  structure LocalSimpset = ProofDataFun
    1.31 -(struct
    1.32 -  val name = "Pure/simpset";
    1.33 +(
    1.34    type T = simpset;
    1.35    val init = get_simpset;
    1.36 -  fun print _ ss = print_ss ss;
    1.37 -end);
    1.38 +);
    1.39  
    1.40 -val _ = Context.add_setup LocalSimpset.init;
    1.41 -val print_local_simpset = LocalSimpset.print;
    1.42 +val print_local_simpset = print_ss o LocalSimpset.get;
    1.43  val get_local_simpset = LocalSimpset.get;
    1.44  val put_local_simpset = LocalSimpset.put;
    1.45  
    1.46 @@ -181,15 +175,12 @@
    1.47  
    1.48  structure Simprocs = GenericDataFun
    1.49  (
    1.50 -  val name = "Pure/simprocs";
    1.51    type T = simproc NameSpace.table;
    1.52    val empty = NameSpace.empty_table;
    1.53    val extend = I;
    1.54    fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
    1.55      handle Symtab.DUPS ds => err_dup_simprocs ds;
    1.56 -  fun print _ _ = ();
    1.57  );
    1.58 -val _ = Context.add_setup Simprocs.init;
    1.59  
    1.60  
    1.61  (* get simprocs *)