# HG changeset patch
# User wenzelm
# Date 1292591377 -3600
# Node ID adcb9a1198e7ba07ad60dbd85bb2449544d7b6a3
# Parent  bd4ecd48c21f3c05128542792fb0939f37f7849a
clarified exports of structure Simplifier;

diff -r bd4ecd48c21f -r adcb9a1198e7 src/HOL/Decision_Procs/langford_data.ML
--- a/src/HOL/Decision_Procs/langford_data.ML	Fri Dec 17 13:45:43 2010 +0100
+++ b/src/HOL/Decision_Procs/langford_data.ML	Fri Dec 17 14:09:37 2010 +0100
@@ -36,11 +36,9 @@
     Thm.declaration_attribute (fn key => fn context => context |> Data.map 
       (del_data key #> apsnd (cons (key, entry))));
 
-val add_simp = Thm.declaration_attribute (fn th => fn context => 
-  context |> Data.map (fn (ss,ts') => (ss addsimps [th], ts'))) 
+val add_simp = Thm.declaration_attribute (Data.map o apfst o Simplifier.add_simp);
 
-val del_simp = Thm.declaration_attribute (fn th => fn context => 
-  context |> Data.map (fn (ss,ts') => (ss delsimps [th], ts'))) 
+val del_simp = Thm.declaration_attribute (Data.map o apfst o Simplifier.del_simp);
 
 fun match ctxt tm =
   let
diff -r bd4ecd48c21f -r adcb9a1198e7 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Dec 17 13:45:43 2010 +0100
+++ b/src/Pure/codegen.ML	Fri Dec 17 14:09:37 2010 +0100
@@ -293,8 +293,8 @@
 );
 
 val map_unfold = UnfoldData.map;
-val add_unfold = map_unfold o MetaSimplifier.add_simp;
-val del_unfold = map_unfold o MetaSimplifier.del_simp;
+val add_unfold = map_unfold o Simplifier.add_simp;
+val del_unfold = map_unfold o Simplifier.del_simp;
 
 fun unfold_preprocessor thy =
   let val ss = Simplifier.global_context thy (UnfoldData.get thy)
diff -r bd4ecd48c21f -r adcb9a1198e7 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Dec 17 13:45:43 2010 +0100
+++ b/src/Pure/meta_simplifier.ML	Fri Dec 17 14:09:37 2010 +0100
@@ -42,7 +42,6 @@
   val make_simproc: {name: string, lhss: cterm list,
     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
   val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
-  val add_prems: thm list -> simpset -> simpset
   val prems_of_ss: simpset -> thm list
   val addsimps: simpset * thm list -> simpset
   val delsimps: simpset * thm list -> simpset
@@ -113,6 +112,7 @@
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc_global: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc
+  val add_prems: thm list -> simpset -> simpset
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
diff -r bd4ecd48c21f -r adcb9a1198e7 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Dec 17 13:45:43 2010 +0100
+++ b/src/Pure/simplifier.ML	Fri Dec 17 14:09:37 2010 +0100
@@ -33,6 +33,9 @@
   val pretty_ss: Proof.context -> simpset -> Pretty.T
   val clear_ss: simpset -> simpset
   val debug_bounds: bool Unsynchronized.ref
+  val add_simp: thm -> simpset -> simpset
+  val del_simp: thm -> simpset -> simpset
+  val add_prems: thm list -> simpset -> simpset
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
diff -r bd4ecd48c21f -r adcb9a1198e7 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Dec 17 13:45:43 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Dec 17 14:09:37 2010 +0100
@@ -83,10 +83,10 @@
 val map_pre = map_pre_post o apfst;
 val map_post = map_pre_post o apsnd;
 
-val add_unfold = map_pre o MetaSimplifier.add_simp;
-val del_unfold = map_pre o MetaSimplifier.del_simp;
-val add_post = map_post o MetaSimplifier.add_simp;
-val del_post = map_post o MetaSimplifier.del_simp;
+val add_unfold = map_pre o Simplifier.add_simp;
+val del_unfold = map_pre o Simplifier.del_simp;
+val add_post = map_post o Simplifier.add_simp;
+val del_post = map_post o Simplifier.del_simp;
 
 fun add_unfold_post raw_thm thy =
   let
@@ -94,7 +94,7 @@
     val thm_sym = Thm.symmetric thm;
   in
     thy |> map_pre_post (fn (pre, post) =>
-      (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.add_simp thm_sym))
+      (pre |> Simplifier.add_simp thm, post |> Simplifier.add_simp thm_sym))
   end;
 
 fun add_functrans (name, f) = (map_data o apsnd)