replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

--- a/src/HOL/Tools/inductive_package.ML	Sat Sep 01 15:46:59 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Sep 01 15:47:01 2007 +0200
@@ -464,8 +464,8 @@
         map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
   in lthy |> note_theorems facts |>> map snd end;
 
-val inductive_cases = gen_inductive_cases Attrib.intern_src ProofContext.read_prop;
-val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
+val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
+val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
 
 
 fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name --
@@ -473,7 +473,7 @@
   #> (fn ((raw_props, fixes), ctxt) =>
     let
       val (_, ctxt') = Variable.add_fixes fixes ctxt;
-      val props = map (ProofContext.read_prop ctxt') raw_props;
+      val props = Syntax.read_props ctxt' raw_props;
       val ctxt'' = fold Variable.declare_term props ctxt';
       val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
     in Method.erule 0 rules end);

--- a/src/HOL/Tools/typedef_package.ML	Sat Sep 01 15:46:59 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Sat Sep 01 15:47:01 2007 +0200
@@ -243,8 +243,8 @@
 
 in
 
-val add_typedef = gen_typedef ProofContext.read_term;
-val add_typedef_i = gen_typedef ProofContext.cert_term;
+val add_typedef = gen_typedef Syntax.read_term;
+val add_typedef_i = gen_typedef Syntax.check_term;
 
 end;
 
@@ -262,8 +262,8 @@
 
 in
 
-val typedef = gen_typedef ProofContext.read_term;
-val typedef_i = gen_typedef ProofContext.cert_term;
+val typedef = gen_typedef Syntax.read_term;
+val typedef_i = gen_typedef Syntax.check_term;
 
 end;
 

--- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Sep 01 15:46:59 2007 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Sep 01 15:47:01 2007 +0200
@@ -173,11 +173,11 @@
     fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
   in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
 
-fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x;
-fun pcpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term true x;
+fun pcpodef_proof x = gen_pcpodef_proof Syntax.read_term true x;
+fun pcpodef_proof_i x = gen_pcpodef_proof Syntax.check_term true x;
 
-fun cpodef_proof x = gen_pcpodef_proof ProofContext.read_term false x;
-fun cpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term false x;
+fun cpodef_proof x = gen_pcpodef_proof Syntax.read_term false x;
+fun cpodef_proof_i x = gen_pcpodef_proof Syntax.check_term false x;
 
 
 (** outer syntax **)

--- a/src/Pure/simplifier.ML	Sat Sep 01 15:46:59 2007 +0200
+++ b/src/Pure/simplifier.ML	Sat Sep 01 15:47:01 2007 +0200
@@ -234,8 +234,8 @@
 
 in
 
-val def_simproc = gen_simproc ProofContext.read_terms;
-val def_simproc_i = gen_simproc ProofContext.cert_terms;
+val def_simproc = gen_simproc Syntax.read_terms;
+val def_simproc_i = gen_simproc Syntax.check_terms;
 
 end;