src/Pure/simplifier.ML
changeset 16458 4c6fd0c01d28
parent 16014 85f4b0f81f62
child 16684 7b58002668c0
     1.1 --- a/src/Pure/simplifier.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4    val mk_context_simproc: string -> cterm list ->
     1.5      (Proof.context -> simpset -> term -> thm option) -> context_simproc
     1.6    val print_simpset: theory -> unit
     1.7 -  val simpset_ref_of_sg: Sign.sg -> simpset ref
     1.8 +  val simpset_ref_of_sg: theory -> simpset ref    (*obsolete*)
     1.9    val simpset_ref_of: theory -> simpset ref
    1.10 -  val simpset_of_sg: Sign.sg -> simpset
    1.11 +  val simpset_of_sg: theory -> simpset            (*obsolete*)
    1.12    val simpset_of: theory -> simpset
    1.13    val SIMPSET: (simpset -> tactic) -> tactic
    1.14    val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
    1.15 @@ -58,13 +58,13 @@
    1.16  signature SIMPLIFIER =
    1.17  sig
    1.18    include BASIC_SIMPLIFIER
    1.19 -  val simproc_i: Sign.sg -> string -> term list
    1.20 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    1.21 -  val simproc: Sign.sg -> string -> string list
    1.22 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    1.23 -  val context_simproc_i: Sign.sg -> string -> term list
    1.24 +  val simproc_i: theory -> string -> term list
    1.25 +    -> (theory -> simpset -> term -> thm option) -> simproc
    1.26 +  val simproc: theory -> string -> string list
    1.27 +    -> (theory -> simpset -> term -> thm option) -> simproc
    1.28 +  val context_simproc_i: theory -> string -> term list
    1.29      -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
    1.30 -  val context_simproc: Sign.sg -> string -> string list
    1.31 +  val context_simproc: theory -> string -> string list
    1.32      -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
    1.33    val          rewrite: simpset -> cterm -> thm
    1.34    val      asm_rewrite: simpset -> cterm -> thm
    1.35 @@ -130,11 +130,11 @@
    1.36  fun eq_context_simproc (ContextSimproc (_, id1), ContextSimproc (_, id2)) = (id1 = id2);
    1.37  val merge_context_simprocs = gen_merge_lists eq_context_simproc;
    1.38  
    1.39 -fun context_simproc_i sg name =
    1.40 -  mk_context_simproc name o map (Thm.cterm_of sg o Logic.varify);
    1.41 +fun context_simproc_i thy name =
    1.42 +  mk_context_simproc name o map (Thm.cterm_of thy o Logic.varify);
    1.43  
    1.44 -fun context_simproc sg name =
    1.45 -  context_simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
    1.46 +fun context_simproc thy name =
    1.47 +  context_simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
    1.48  
    1.49  
    1.50  (* datatype context_ss *)
    1.51 @@ -188,25 +188,24 @@
    1.52  
    1.53  (* theory data kind 'Pure/simpset' *)
    1.54  
    1.55 -structure GlobalSimpsetArgs =
    1.56 -struct
    1.57 +structure GlobalSimpset = TheoryDataFun
    1.58 +(struct
    1.59    val name = "Pure/simpset";
    1.60    type T = simpset ref * context_ss;
    1.61  
    1.62    val empty = (ref empty_ss, empty_context_ss);
    1.63    fun copy (ref ss, ctxt_ss) = (ref ss, ctxt_ss): T;            (*create new reference!*)
    1.64 -  val prep_ext = copy;
    1.65 -  fun merge ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =
    1.66 +  val extend = copy;
    1.67 +  fun merge _ ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =
    1.68      (ref (merge_ss (ss1, ss2)), merge_context_ss (ctxt_ss1, ctxt_ss2));
    1.69    fun print _ (ref ss, _) = print_ss ss;
    1.70 -end;
    1.71 +end);
    1.72  
    1.73 -structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
    1.74  val _ = Context.add_setup [GlobalSimpset.init];
    1.75  val print_simpset = GlobalSimpset.print;
    1.76  
    1.77 -val simpset_ref_of_sg = #1 o GlobalSimpset.get_sg;
    1.78  val simpset_ref_of = #1 o GlobalSimpset.get;
    1.79 +val simpset_ref_of_sg = simpset_ref_of;
    1.80  val get_context_ss = #2 o GlobalSimpset.get o ProofContext.theory_of;
    1.81  
    1.82  fun map_context_ss f = GlobalSimpset.map (apsnd
    1.83 @@ -216,14 +215,14 @@
    1.84  
    1.85  (* access global simpset *)
    1.86  
    1.87 -val simpset_of_sg = ! o simpset_ref_of_sg;
    1.88 -val simpset_of = simpset_of_sg o Theory.sign_of;
    1.89 +val simpset_of = ! o simpset_ref_of;
    1.90 +val simpset_of_sg = simpset_of;
    1.91  
    1.92 -fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
    1.93 -fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
    1.94 +fun SIMPSET tacf state = tacf (simpset_of (Thm.theory_of_thm state)) state;
    1.95 +fun SIMPSET' tacf i state = tacf (simpset_of (Thm.theory_of_thm state)) i state;
    1.96  
    1.97  val simpset = simpset_of o Context.the_context;
    1.98 -val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
    1.99 +val simpset_ref = simpset_ref_of o Context.the_context;
   1.100  
   1.101  
   1.102  (* change global simpset *)
   1.103 @@ -285,15 +284,14 @@
   1.104  
   1.105  (* proof data kind 'Pure/simpset' *)
   1.106  
   1.107 -structure LocalSimpsetArgs =
   1.108 -struct
   1.109 +structure LocalSimpset = ProofDataFun
   1.110 +(struct
   1.111    val name = "Pure/simpset";
   1.112    type T = simpset;
   1.113    val init = simpset_of;
   1.114    fun print ctxt ss = print_ss (context_ss ctxt ss (get_context_ss ctxt));
   1.115 -end;
   1.116 +end);
   1.117  
   1.118 -structure LocalSimpset = ProofDataFun(LocalSimpsetArgs);
   1.119  val _ = Context.add_setup [LocalSimpset.init];
   1.120  val print_local_simpset = LocalSimpset.print;
   1.121