# HG changeset patch
# User haftmann
# Date 1247581653 -7200
# Node ID b4a48533ce0c9627faf59757188d00f112b73ab4
# Parent  c670a31c964cf9aec17b3a7938108b01b52b4a40
more accessors to unfold simpset

diff -r c670a31c964c -r b4a48533ce0c src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Jul 14 16:27:33 2009 +0200
+++ b/src/Pure/codegen.ML	Tue Jul 14 16:27:33 2009 +0200
@@ -85,7 +85,9 @@
   val num_args_of: 'a mixfix list -> int
   val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
   val mk_deftab: theory -> deftab
+  val map_unfold: (simpset -> simpset) -> theory -> theory
   val add_unfold: thm -> theory -> theory
+  val del_unfold: thm -> theory -> theory
 
   val get_node: codegr -> string -> node
   val add_edge: string * string -> codegr -> codegr
@@ -296,13 +298,9 @@
   fun merge _ = merge_ss;
 );
 
-fun add_unfold eqn =
-  let
-    val ctxt = ProofContext.init (Thm.theory_of_thm eqn);
-    val eqn' = LocalDefs.meta_rewrite_rule ctxt eqn;
-  in
-    UnfoldData.map (fn ss => ss addsimps [eqn'])
-  end;
+val map_unfold = UnfoldData.map;
+val add_unfold = map_unfold o MetaSimplifier.add_simp;
+val del_unfold = map_unfold o MetaSimplifier.del_simp;
 
 fun unfold_preprocessor thy =
   let val ss = Simplifier.theory_context thy (UnfoldData.get thy)