1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Sep 01 15:46:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Sep 01 15:47:01 2007 +0200
     1.3 @@ -464,8 +464,8 @@
     1.4          map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
     1.5    in lthy |> note_theorems facts |>> map snd end;
     1.6  
     1.7 -val inductive_cases = gen_inductive_cases Attrib.intern_src ProofContext.read_prop;
     1.8 -val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
     1.9 +val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    1.10 +val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    1.11  
    1.12  
    1.13  fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name --
    1.14 @@ -473,7 +473,7 @@
    1.15    #> (fn ((raw_props, fixes), ctxt) =>
    1.16      let
    1.17        val (_, ctxt') = Variable.add_fixes fixes ctxt;
    1.18 -      val props = map (ProofContext.read_prop ctxt') raw_props;
    1.19 +      val props = Syntax.read_props ctxt' raw_props;
    1.20        val ctxt'' = fold Variable.declare_term props ctxt';
    1.21        val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
    1.22      in Method.erule 0 rules end);

     2.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Sep 01 15:46:59 2007 +0200
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Sep 01 15:47:01 2007 +0200
     2.3 @@ -243,8 +243,8 @@
     2.4  
     2.5  in
     2.6  
     2.7 -val add_typedef = gen_typedef ProofContext.read_term;
     2.8 -val add_typedef_i = gen_typedef ProofContext.cert_term;
     2.9 +val add_typedef = gen_typedef Syntax.read_term;
    2.10 +val add_typedef_i = gen_typedef Syntax.check_term;
    2.11  
    2.12  end;
    2.13  
    2.14 @@ -262,8 +262,8 @@
    2.15  
    2.16  in
    2.17  
    2.18 -val typedef = gen_typedef ProofContext.read_term;
    2.19 -val typedef_i = gen_typedef ProofContext.cert_term;
    2.20 +val typedef = gen_typedef Syntax.read_term;
    2.21 +val typedef_i = gen_typedef Syntax.check_term;
    2.22  
    2.23  end;
    2.24  

     3.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Sep 01 15:46:59 2007 +0200
     3.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Sep 01 15:47:01 2007 +0200
     3.3 @@ -173,11 +173,11 @@
     3.4      fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
     3.5    in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
     3.6  
     3.7 -fun pcpodef_proof x = gen_pcpodef_proof ProofContext.read_term true x;
     3.8 -fun pcpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term true x;
     3.9 +fun pcpodef_proof x = gen_pcpodef_proof Syntax.read_term true x;
    3.10 +fun pcpodef_proof_i x = gen_pcpodef_proof Syntax.check_term true x;
    3.11  
    3.12 -fun cpodef_proof x = gen_pcpodef_proof ProofContext.read_term false x;
    3.13 -fun cpodef_proof_i x = gen_pcpodef_proof ProofContext.cert_term false x;
    3.14 +fun cpodef_proof x = gen_pcpodef_proof Syntax.read_term false x;
    3.15 +fun cpodef_proof_i x = gen_pcpodef_proof Syntax.check_term false x;
    3.16  
    3.17  
    3.18  (** outer syntax **)

     4.1 --- a/src/Pure/simplifier.ML	Sat Sep 01 15:46:59 2007 +0200
     4.2 +++ b/src/Pure/simplifier.ML	Sat Sep 01 15:47:01 2007 +0200
     4.3 @@ -234,8 +234,8 @@
     4.4  
     4.5  in
     4.6  
     4.7 -val def_simproc = gen_simproc ProofContext.read_terms;
     4.8 -val def_simproc_i = gen_simproc ProofContext.cert_terms;
     4.9 +val def_simproc = gen_simproc Syntax.read_terms;
    4.10 +val def_simproc_i = gen_simproc Syntax.check_terms;
    4.11  
    4.12  end;
    4.13