replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
authorwenzelm
Sat Sep 01 15:46:59 2007 +0200 (2007-09-01)
changeset 24508c8b82fec6447
parent 24507 ac22a2a67100
child 24509 23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
src/HOL/Library/Eval.thy
src/HOL/Tools/function_package/fundef_package.ML
src/Pure/Isar/args.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Tools/nbe.ML
src/Pure/codegen.ML
src/Tools/nbe.ML
src/ZF/Tools/ind_cases.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Sat Sep 01 01:22:11 2007 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Sat Sep 01 15:46:59 2007 +0200
     1.3 @@ -207,7 +207,7 @@
     1.4  fun eval_print_cmd conv raw_t state =
     1.5    let
     1.6      val ctxt = Toplevel.context_of state;
     1.7 -    val t = ProofContext.read_term ctxt raw_t;
     1.8 +    val t = Syntax.read_term ctxt raw_t;
     1.9      val thy = ProofContext.theory_of ctxt;
    1.10      val ct = Thm.cterm_of thy t;
    1.11      val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Sep 01 01:22:11 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Sep 01 15:46:59 2007 +0200
     2.3 @@ -144,7 +144,7 @@
     2.4  fun setup_termination_proof term_opt lthy =
     2.5      let
     2.6        val data = the (case term_opt of
     2.7 -                        SOME t => import_fundef_data (ProofContext.read_term lthy t) (Context.Proof lthy)
     2.8 +                        SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy)
     2.9                        | NONE => import_last_fundef (Context.Proof lthy))
    2.10            handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt))
    2.11  
     3.1 --- a/src/Pure/Isar/args.ML	Sat Sep 01 01:22:11 2007 +0200
     3.2 +++ b/src/Pure/Isar/args.ML	Sat Sep 01 15:46:59 2007 +0200
     3.3 @@ -323,9 +323,9 @@
     3.4  
     3.5  val typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o Context.proof_of);
     3.6  val typ = Scan.peek (named_typ o ProofContext.read_typ o Context.proof_of);
     3.7 -val term = Scan.peek (named_term o ProofContext.read_term o Context.proof_of);
     3.8 +val term = Scan.peek (named_term o Syntax.read_term o Context.proof_of);
     3.9  val term_abbrev = Scan.peek (named_term o ProofContext.read_term_abbrev o Context.proof_of);
    3.10 -val prop = Scan.peek (named_term o ProofContext.read_prop o Context.proof_of);
    3.11 +val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of);
    3.12  
    3.13  
    3.14  (* type and constant names *)
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Sep 01 01:22:11 2007 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Sep 01 15:46:59 2007 +0200
     4.3 @@ -563,13 +563,13 @@
     4.4  fun string_of_prop state s =
     4.5    let
     4.6      val ctxt = Proof.context_of state;
     4.7 -    val prop = ProofContext.read_prop ctxt s;
     4.8 +    val prop = Syntax.read_prop ctxt s;
     4.9    in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end;
    4.10  
    4.11  fun string_of_term state s =
    4.12    let
    4.13      val ctxt = Proof.context_of state;
    4.14 -    val t = ProofContext.read_term ctxt s;
    4.15 +    val t = Syntax.read_term ctxt s;
    4.16      val T = Term.type_of t;
    4.17    in
    4.18      Pretty.string_of
     5.1 --- a/src/Pure/Tools/nbe.ML	Sat Sep 01 01:22:11 2007 +0200
     5.2 +++ b/src/Pure/Tools/nbe.ML	Sat Sep 01 15:46:59 2007 +0200
     5.3 @@ -195,9 +195,9 @@
     5.4          Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
     5.5    in Pretty.writeln p end;
     5.6  
     5.7 -fun norm_print_term_e (modes, raw_t) state =
     5.8 +fun norm_print_term_e (modes, s) state =
     5.9    let val ctxt = Toplevel.context_of state
    5.10 -  in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end;
    5.11 +  in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
    5.12  
    5.13  val _ = Context.add_setup
    5.14    (Theory.add_oracle ("normalization", normalization_oracle));
     6.1 --- a/src/Pure/codegen.ML	Sat Sep 01 01:22:11 2007 +0200
     6.2 +++ b/src/Pure/codegen.ML	Sat Sep 01 15:46:59 2007 +0200
     6.3 @@ -1024,7 +1024,7 @@
     6.4    let
     6.5      val ctxt = Toplevel.context_of state;
     6.6      val thy = ProofContext.theory_of ctxt;
     6.7 -    val t = eval_term thy (ProofContext.read_term ctxt s);
     6.8 +    val t = eval_term thy (Syntax.read_term ctxt s);
     6.9      val T = Term.type_of t;
    6.10    in
    6.11      writeln (Pretty.string_of
     7.1 --- a/src/Tools/nbe.ML	Sat Sep 01 01:22:11 2007 +0200
     7.2 +++ b/src/Tools/nbe.ML	Sat Sep 01 15:46:59 2007 +0200
     7.3 @@ -377,9 +377,9 @@
     7.4  
     7.5  (** Isar setup **)
     7.6  
     7.7 -fun norm_print_term_cmd (modes, raw_t) state =
     7.8 +fun norm_print_term_cmd (modes, s) state =
     7.9    let val ctxt = Toplevel.context_of state
    7.10 -  in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end;
    7.11 +  in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
    7.12  
    7.13  val setup = Theory.add_oracle ("normalization", normalization_oracle)
    7.14  
     8.1 --- a/src/ZF/Tools/ind_cases.ML	Sat Sep 01 01:22:11 2007 +0200
     8.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Sep 01 15:46:59 2007 +0200
     8.3 @@ -47,7 +47,7 @@
     8.4  
     8.5  fun inductive_cases args thy =
     8.6    let
     8.7 -    val read_prop = ProofContext.read_prop (ProofContext.init thy);
     8.8 +    val read_prop = Syntax.read_prop (ProofContext.init thy);
     8.9      val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
    8.10      val facts = args |> map (fn ((name, srcs), props) =>
    8.11        ((name, map (Attrib.attribute thy) srcs),
    8.12 @@ -59,8 +59,7 @@
    8.13  
    8.14  fun mk_cases_meth (props, ctxt) =
    8.15    props
    8.16 -  |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt)
    8.17 -    (ProofContext.read_prop ctxt))
    8.18 +  |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
    8.19    |> Method.erule 0;
    8.20  
    8.21  val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));