tuned signature;
authorwenzelm
Sun Mar 09 16:37:56 2014 +0100 (2014-03-09)
changeset 560022028467b4df4
parent 56001 2df1e7bca361
child 56003 eccac152ffb4
tuned signature;
src/Doc/ProgProve/LaTeXsugar.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Quickcheck/abstract_generators.ML
src/Pure/Isar/args.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/thy_output.ML
src/Tools/Code/code_target.ML
src/Tools/adhoc_overloading.ML
     1.1 --- a/src/Doc/ProgProve/LaTeXsugar.thy	Sun Mar 09 15:21:08 2014 +0100
     1.2 +++ b/src/Doc/ProgProve/LaTeXsugar.thy	Sun Mar 09 16:37:56 2014 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4  setup{*
     1.5    let
     1.6      fun pretty ctxt c =
     1.7 -      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c
     1.8 +      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
     1.9        in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    1.10              Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
    1.11        end
     2.1 --- a/src/HOL/Library/LaTeXsugar.thy	Sun Mar 09 15:21:08 2014 +0100
     2.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Sun Mar 09 16:37:56 2014 +0100
     2.3 @@ -100,7 +100,7 @@
     2.4  setup{*
     2.5    let
     2.6      fun pretty ctxt c =
     2.7 -      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c
     2.8 +      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
     2.9        in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    2.10              Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
    2.11        end
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sun Mar 09 15:21:08 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sun Mar 09 16:37:56 2014 +0100
     3.3 @@ -33,7 +33,7 @@
     3.4        error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
     3.5  
     3.6      val fpT_names =
     3.7 -      map (fst o dest_Type o Proof_Context.read_type_name lthy {proper = true, strict = false})
     3.8 +      map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy)
     3.9          raw_fpT_names;
    3.10  
    3.11      fun lfp_sugar_of s =
     4.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sun Mar 09 15:21:08 2014 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sun Mar 09 16:37:56 2014 +0100
     4.3 @@ -535,9 +535,9 @@
     4.4  
     4.5      val ctxt = Proof_Context.init_global thy9;
     4.6      val case_combs =
     4.7 -      map (Proof_Context.read_const ctxt {proper = true, strict = true}) case_names;
     4.8 +      map (Proof_Context.read_const {proper = true, strict = true} ctxt) case_names;
     4.9      val constrss = map (fn (dtname, {descr, index, ...}) =>
    4.10 -      map (Proof_Context.read_const ctxt {proper = true, strict = true} o fst)
    4.11 +      map (Proof_Context.read_const {proper = true, strict = true} ctxt o fst)
    4.12          (#3 (the (AList.lookup op = descr index)))) dt_infos;
    4.13    in
    4.14      thy9
     5.1 --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Sun Mar 09 15:21:08 2014 +0100
     5.2 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Sun Mar 09 16:37:56 2014 +0100
     5.3 @@ -63,7 +63,7 @@
     5.4    
     5.5  val quickcheck_generator_cmd =
     5.6    gen_quickcheck_generator
     5.7 -    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true})
     5.8 +    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = true})
     5.9      Syntax.read_term
    5.10    
    5.11  val _ =
     6.1 --- a/src/Pure/Isar/args.ML	Sun Mar 09 15:21:08 2014 +0100
     6.2 +++ b/src/Pure/Isar/args.ML	Sun Mar 09 16:37:56 2014 +0100
     6.3 @@ -208,11 +208,11 @@
     6.4  (* type and constant names *)
     6.5  
     6.6  fun type_name flags =
     6.7 -  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
     6.8 +  Scan.peek (named_typ o Proof_Context.read_type_name flags o Context.proof_of)
     6.9    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
    6.10  
    6.11  fun const flags =
    6.12 -  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags))
    6.13 +  Scan.peek (named_term o Proof_Context.read_const flags o Context.proof_of)
    6.14    >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
    6.15  
    6.16  
     7.1 --- a/src/Pure/Isar/proof.ML	Sun Mar 09 15:21:08 2014 +0100
     7.2 +++ b/src/Pure/Isar/proof.ML	Sun Mar 09 16:37:56 2014 +0100
     7.3 @@ -575,7 +575,7 @@
     7.4    #> reset_facts;
     7.5  
     7.6  fun read_arg ctxt (c, mx) =
     7.7 -  (case Proof_Context.read_const ctxt {proper = false, strict = false} c of
     7.8 +  (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
     7.9      Free (x, _) =>
    7.10        let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
    7.11        in (Free (x, T), mx) end
     8.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 09 15:21:08 2014 +0100
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 09 16:37:56 2014 +0100
     8.3 @@ -68,13 +68,13 @@
     8.4    val infer_type: Proof.context -> string * typ -> typ
     8.5    val inferred_param: string -> Proof.context -> typ * Proof.context
     8.6    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
     8.7 -  val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     8.8 +  val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
     8.9      xstring * Position.T -> typ * Position.report list
    8.10 -  val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
    8.11 +  val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ
    8.12    val consts_completion_message: Proof.context -> xstring * Position.T list -> string
    8.13 -  val check_const: Proof.context -> {proper: bool, strict: bool} ->
    8.14 +  val check_const: {proper: bool, strict: bool} -> Proof.context ->
    8.15      xstring * Position.T list -> term * Position.report list
    8.16 -  val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
    8.17 +  val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term
    8.18    val read_arity: Proof.context -> xstring * string list * string -> arity
    8.19    val cert_arity: Proof.context -> arity -> arity
    8.20    val allow_dummies: Proof.context -> Proof.context
    8.21 @@ -439,7 +439,7 @@
    8.22  
    8.23  (* type names *)
    8.24  
    8.25 -fun check_type_name ctxt {proper, strict} (c, pos) =
    8.26 +fun check_type_name {proper, strict} ctxt (c, pos) =
    8.27    if Lexicon.is_tid c then
    8.28      if proper then error ("Not a type constructor: " ^ c ^ Position.here pos)
    8.29      else
    8.30 @@ -476,7 +476,7 @@
    8.31    |> implode
    8.32    |> Markup.markup_report;
    8.33  
    8.34 -fun check_const ctxt {proper, strict} (c, ps) =
    8.35 +fun check_const {proper, strict} ctxt (c, ps) =
    8.36    let
    8.37      val _ =
    8.38        Name.reject_internal (c, ps) handle ERROR msg =>
    8.39 @@ -527,8 +527,7 @@
    8.40  in
    8.41  
    8.42  val read_arity =
    8.43 -  prep_arity (fn ctxt => #1 o dest_Type o read_type_name ctxt {proper = true, strict = true})
    8.44 -    Syntax.read_sort;
    8.45 +  prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort;
    8.46  
    8.47  val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
    8.48  
     9.1 --- a/src/Pure/Isar/specification.ML	Sun Mar 09 15:21:08 2014 +0100
     9.2 +++ b/src/Pure/Isar/specification.ML	Sun Mar 09 16:37:56 2014 +0100
     9.3 @@ -275,11 +275,10 @@
     9.4  
     9.5  val type_notation = gen_type_notation (K I);
     9.6  val type_notation_cmd =
     9.7 -  gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = true, strict = false});
     9.8 +  gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
     9.9  
    9.10  val notation = gen_notation (K I);
    9.11 -val notation_cmd =
    9.12 -  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false});
    9.13 +val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
    9.14  
    9.15  end;
    9.16  
    10.1 --- a/src/Pure/ML/ml_antiquote.ML	Sun Mar 09 15:21:08 2014 +0100
    10.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sun Mar 09 16:37:56 2014 +0100
    10.3 @@ -127,7 +127,7 @@
    10.4  fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
    10.5    >> (fn (ctxt, (s, pos)) =>
    10.6      let
    10.7 -      val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s;
    10.8 +      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
    10.9        val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
   10.10        val res =
   10.11          (case try check (c, decl) of
   10.12 @@ -151,7 +151,7 @@
   10.13  fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   10.14    >> (fn (ctxt, (s, pos)) =>
   10.15      let
   10.16 -      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} s;
   10.17 +      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
   10.18        val res = check (Proof_Context.consts_of ctxt, c)
   10.19          handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   10.20      in ML_Syntax.print_string res end);
   10.21 @@ -176,7 +176,7 @@
   10.22        >> (fn ((ctxt, raw_c), Ts) =>
   10.23          let
   10.24            val Const (c, _) =
   10.25 -            Proof_Context.read_const ctxt {proper = true, strict = true} raw_c;
   10.26 +            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
   10.27            val consts = Proof_Context.consts_of ctxt;
   10.28            val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
   10.29            val _ = length Ts <> n andalso
    11.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun Mar 09 15:21:08 2014 +0100
    11.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Mar 09 16:37:56 2014 +0100
    11.3 @@ -171,7 +171,7 @@
    11.4            let
    11.5              val pos = Lexicon.pos_of_token tok;
    11.6              val (Type (c, _), rs) =
    11.7 -              Proof_Context.check_type_name ctxt {proper = true, strict = false}
    11.8 +              Proof_Context.check_type_name {proper = true, strict = false} ctxt
    11.9                  (Lexicon.str_of_token tok, pos);
   11.10              val _ = append_reports rs;
   11.11            in [Ast.Constant (Lexicon.mark_type c)] end
   11.12 @@ -225,7 +225,7 @@
   11.13  fun decode_const ctxt (c, ps) =
   11.14    let
   11.15      val (Const (c', _), reports) =
   11.16 -      Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
   11.17 +      Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps);
   11.18    in (c', reports) end;
   11.19  
   11.20  local
    12.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 09 15:21:08 2014 +0100
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 09 16:37:56 2014 +0100
    12.3 @@ -515,7 +515,7 @@
    12.4    Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
    12.5  
    12.6  fun pretty_type ctxt s =
    12.7 -  let val Type (name, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s
    12.8 +  let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
    12.9    in Pretty.str (Proof_Context.extern_type ctxt name) end;
   12.10  
   12.11  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
    13.1 --- a/src/Tools/Code/code_target.ML	Sun Mar 09 15:21:08 2014 +0100
    13.2 +++ b/src/Tools/Code/code_target.ML	Sun Mar 09 16:37:56 2014 +0100
    13.3 @@ -98,7 +98,7 @@
    13.4    in tyco end;
    13.5  
    13.6  fun read_tyco ctxt =
    13.7 -  #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true};
    13.8 +  #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt;
    13.9  
   13.10  fun cert_class ctxt class =
   13.11    let
    14.1 --- a/src/Tools/adhoc_overloading.ML	Sun Mar 09 15:21:08 2014 +0100
    14.2 +++ b/src/Tools/adhoc_overloading.ML	Sun Mar 09 16:37:56 2014 +0100
    14.3 @@ -221,7 +221,7 @@
    14.4  fun adhoc_overloading_cmd add raw_args lthy =
    14.5    let
    14.6      fun const_name ctxt =
    14.7 -      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};  (* FIXME {proper = true, strict = true} (!?) *)
    14.8 +      fst o dest_Const o Proof_Context.read_const {proper = false, strict = false} ctxt;  (* FIXME {proper = true, strict = true} (!?) *)
    14.9      fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
   14.10      val args =
   14.11        raw_args