replaced ProofContext.read_term/prop by general Syntax.read_term/prop;

--- a/src/HOL/Library/Eval.thy	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Sat Sep 01 15:46:59 2007 +0200
@@ -207,7 +207,7 @@
 fun eval_print_cmd conv raw_t state =
   let
     val ctxt = Toplevel.context_of state;
-    val t = ProofContext.read_term ctxt raw_t;
+    val t = Syntax.read_term ctxt raw_t;
     val thy = ProofContext.theory_of ctxt;
     val ct = Thm.cterm_of thy t;
     val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;

--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Sep 01 15:46:59 2007 +0200
@@ -144,7 +144,7 @@
 fun setup_termination_proof term_opt lthy =
     let
       val data = the (case term_opt of
-                        SOME t => import_fundef_data (ProofContext.read_term lthy t) (Context.Proof lthy)
+                        SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy)
                       | NONE => import_last_fundef (Context.Proof lthy))
           handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt))
 

--- a/src/Pure/Isar/args.ML	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/Pure/Isar/args.ML	Sat Sep 01 15:46:59 2007 +0200
@@ -323,9 +323,9 @@
 
 val typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o Context.proof_of);
 val typ = Scan.peek (named_typ o ProofContext.read_typ o Context.proof_of);
-val term = Scan.peek (named_term o ProofContext.read_term o Context.proof_of);
+val term = Scan.peek (named_term o Syntax.read_term o Context.proof_of);
 val term_abbrev = Scan.peek (named_term o ProofContext.read_term_abbrev o Context.proof_of);
-val prop = Scan.peek (named_term o ProofContext.read_prop o Context.proof_of);
+val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of);
 
 
 (* type and constant names *)

--- a/src/Pure/Isar/isar_cmd.ML	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Sep 01 15:46:59 2007 +0200
@@ -563,13 +563,13 @@
 fun string_of_prop state s =
   let
     val ctxt = Proof.context_of state;
-    val prop = ProofContext.read_prop ctxt s;
+    val prop = Syntax.read_prop ctxt s;
   in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end;
 
 fun string_of_term state s =
   let
     val ctxt = Proof.context_of state;
-    val t = ProofContext.read_term ctxt s;
+    val t = Syntax.read_term ctxt s;
     val T = Term.type_of t;
   in
     Pretty.string_of

--- a/src/Pure/Tools/nbe.ML	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/Pure/Tools/nbe.ML	Sat Sep 01 15:46:59 2007 +0200
@@ -195,9 +195,9 @@
         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
   in Pretty.writeln p end;
 
-fun norm_print_term_e (modes, raw_t) state =
+fun norm_print_term_e (modes, s) state =
   let val ctxt = Toplevel.context_of state
-  in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end;
+  in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
 
 val _ = Context.add_setup
   (Theory.add_oracle ("normalization", normalization_oracle));

--- a/src/Pure/codegen.ML	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/Pure/codegen.ML	Sat Sep 01 15:46:59 2007 +0200
@@ -1024,7 +1024,7 @@
   let
     val ctxt = Toplevel.context_of state;
     val thy = ProofContext.theory_of ctxt;
-    val t = eval_term thy (ProofContext.read_term ctxt s);
+    val t = eval_term thy (Syntax.read_term ctxt s);
     val T = Term.type_of t;
   in
     writeln (Pretty.string_of

--- a/src/Tools/nbe.ML	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/Tools/nbe.ML	Sat Sep 01 15:46:59 2007 +0200
@@ -377,9 +377,9 @@
 
 (** Isar setup **)
 
-fun norm_print_term_cmd (modes, raw_t) state =
+fun norm_print_term_cmd (modes, s) state =
   let val ctxt = Toplevel.context_of state
-  in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end;
+  in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
 
 val setup = Theory.add_oracle ("normalization", normalization_oracle)
 

--- a/src/ZF/Tools/ind_cases.ML	Sat Sep 01 01:22:11 2007 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Sat Sep 01 15:46:59 2007 +0200
@@ -47,7 +47,7 @@
 
 fun inductive_cases args thy =
   let
-    val read_prop = ProofContext.read_prop (ProofContext.init thy);
+    val read_prop = Syntax.read_prop (ProofContext.init thy);
     val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
     val facts = args |> map (fn ((name, srcs), props) =>
       ((name, map (Attrib.attribute thy) srcs),
@@ -59,8 +59,7 @@
 
 fun mk_cases_meth (props, ctxt) =
   props
-  |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt)
-    (ProofContext.read_prop ctxt))
+  |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
   |> Method.erule 0;
 
 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));