# HG changeset patch
# User wenzelm
# Date 1177353849 -7200
# Node ID 615e19792c928af135ef3c2fb26e05e6b127122e
# Parent  6f5068e26b8935d61f25d61bb5096ae3e08d983b
def_simproc(_i): proper ProofContext.read/cert_terms;

diff -r 6f5068e26b89 -r 615e19792c92 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Mon Apr 23 20:44:08 2007 +0200
+++ b/src/Pure/simplifier.ML	Mon Apr 23 20:44:09 2007 +0200
@@ -213,14 +213,6 @@
 
 local
 
-(* FIXME *)
-fun read_terms ctxt ts =
-  #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) []
-    (map (rpair dummyT) ts));
-
-(* FIXME *)
-fun cert_terms ctxt ts = map (ProofContext.cert_term ctxt) ts;
-
 fun gen_simproc prep {name, lhss, proc, identifier} lthy =
   let
     val naming = LocalTheory.full_naming lthy;
@@ -253,8 +245,8 @@
 
 in
 
-val def_simproc = gen_simproc read_terms;
-val def_simproc_i = gen_simproc cert_terms;
+val def_simproc = gen_simproc ProofContext.read_terms;
+val def_simproc_i = gen_simproc ProofContext.cert_terms;
 
 end;