# HG changeset patch
# User wenzelm
# Date 1394379476 -3600
# Node ID 2028467b4df4e26bd4dedfb1b06484adc0f93582
# Parent  2df1e7bca361af0e1e9af12319e1661dc914bc16
tuned signature;

diff -r 2df1e7bca361 -r 2028467b4df4 src/Doc/ProgProve/LaTeXsugar.thy
--- a/src/Doc/ProgProve/LaTeXsugar.thy	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy	Sun Mar 09 16:37:56 2014 +0100
@@ -46,7 +46,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c
+      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end
diff -r 2df1e7bca361 -r 2028467b4df4 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Sun Mar 09 16:37:56 2014 +0100
@@ -100,7 +100,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c
+      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end
diff -r 2df1e7bca361 -r 2028467b4df4 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -33,7 +33,7 @@
       error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
 
     val fpT_names =
-      map (fst o dest_Type o Proof_Context.read_type_name lthy {proper = true, strict = false})
+      map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy)
         raw_fpT_names;
 
     fun lfp_sugar_of s =
diff -r 2df1e7bca361 -r 2028467b4df4 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -535,9 +535,9 @@
 
     val ctxt = Proof_Context.init_global thy9;
     val case_combs =
-      map (Proof_Context.read_const ctxt {proper = true, strict = true}) case_names;
+      map (Proof_Context.read_const {proper = true, strict = true} ctxt) case_names;
     val constrss = map (fn (dtname, {descr, index, ...}) =>
-      map (Proof_Context.read_const ctxt {proper = true, strict = true} o fst)
+      map (Proof_Context.read_const {proper = true, strict = true} ctxt o fst)
         (#3 (the (AList.lookup op = descr index)))) dt_infos;
   in
     thy9
diff -r 2df1e7bca361 -r 2028467b4df4 src/HOL/Tools/Quickcheck/abstract_generators.ML
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -63,7 +63,7 @@
   
 val quickcheck_generator_cmd =
   gen_quickcheck_generator
-    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true})
+    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = true})
     Syntax.read_term
   
 val _ =
diff -r 2df1e7bca361 -r 2028467b4df4 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Pure/Isar/args.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -208,11 +208,11 @@
 (* type and constant names *)
 
 fun type_name flags =
-  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
+  Scan.peek (named_typ o Proof_Context.read_type_name flags o Context.proof_of)
   >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
 fun const flags =
-  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags))
+  Scan.peek (named_term o Proof_Context.read_const flags o Context.proof_of)
   >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
 
diff -r 2df1e7bca361 -r 2028467b4df4 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -575,7 +575,7 @@
   #> reset_facts;
 
 fun read_arg ctxt (c, mx) =
-  (case Proof_Context.read_const ctxt {proper = false, strict = false} c of
+  (case Proof_Context.read_const {proper = false, strict = false} ctxt c of
     Free (x, _) =>
       let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
       in (Free (x, T), mx) end
diff -r 2df1e7bca361 -r 2028467b4df4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -68,13 +68,13 @@
   val infer_type: Proof.context -> string * typ -> typ
   val inferred_param: string -> Proof.context -> typ * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
-  val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
+  val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
     xstring * Position.T -> typ * Position.report list
-  val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
+  val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ
   val consts_completion_message: Proof.context -> xstring * Position.T list -> string
-  val check_const: Proof.context -> {proper: bool, strict: bool} ->
+  val check_const: {proper: bool, strict: bool} -> Proof.context ->
     xstring * Position.T list -> term * Position.report list
-  val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
+  val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term
   val read_arity: Proof.context -> xstring * string list * string -> arity
   val cert_arity: Proof.context -> arity -> arity
   val allow_dummies: Proof.context -> Proof.context
@@ -439,7 +439,7 @@
 
 (* type names *)
 
-fun check_type_name ctxt {proper, strict} (c, pos) =
+fun check_type_name {proper, strict} ctxt (c, pos) =
   if Lexicon.is_tid c then
     if proper then error ("Not a type constructor: " ^ c ^ Position.here pos)
     else
@@ -476,7 +476,7 @@
   |> implode
   |> Markup.markup_report;
 
-fun check_const ctxt {proper, strict} (c, ps) =
+fun check_const {proper, strict} ctxt (c, ps) =
   let
     val _ =
       Name.reject_internal (c, ps) handle ERROR msg =>
@@ -527,8 +527,7 @@
 in
 
 val read_arity =
-  prep_arity (fn ctxt => #1 o dest_Type o read_type_name ctxt {proper = true, strict = true})
-    Syntax.read_sort;
+  prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort;
 
 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
 
diff -r 2df1e7bca361 -r 2028467b4df4 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -275,11 +275,10 @@
 
 val type_notation = gen_type_notation (K I);
 val type_notation_cmd =
-  gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = true, strict = false});
+  gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
 
 val notation = gen_notation (K I);
-val notation_cmd =
-  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false});
+val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
 
 end;
 
diff -r 2df1e7bca361 -r 2028467b4df4 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -127,7 +127,7 @@
 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s;
+      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
       val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
       val res =
         (case try check (c, decl) of
@@ -151,7 +151,7 @@
 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   >> (fn (ctxt, (s, pos)) =>
     let
-      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} s;
+      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
       val res = check (Proof_Context.consts_of ctxt, c)
         handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
     in ML_Syntax.print_string res end);
@@ -176,7 +176,7 @@
       >> (fn ((ctxt, raw_c), Ts) =>
         let
           val Const (c, _) =
-            Proof_Context.read_const ctxt {proper = true, strict = true} raw_c;
+            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
           val consts = Proof_Context.consts_of ctxt;
           val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
           val _ = length Ts <> n andalso
diff -r 2df1e7bca361 -r 2028467b4df4 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -171,7 +171,7 @@
           let
             val pos = Lexicon.pos_of_token tok;
             val (Type (c, _), rs) =
-              Proof_Context.check_type_name ctxt {proper = true, strict = false}
+              Proof_Context.check_type_name {proper = true, strict = false} ctxt
                 (Lexicon.str_of_token tok, pos);
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
@@ -225,7 +225,7 @@
 fun decode_const ctxt (c, ps) =
   let
     val (Const (c', _), reports) =
-      Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
+      Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps);
   in (c', reports) end;
 
 local
diff -r 2df1e7bca361 -r 2028467b4df4 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -515,7 +515,7 @@
   Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
 
 fun pretty_type ctxt s =
-  let val Type (name, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s
+  let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
   in Pretty.str (Proof_Context.extern_type ctxt name) end;
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
diff -r 2df1e7bca361 -r 2028467b4df4 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -98,7 +98,7 @@
   in tyco end;
 
 fun read_tyco ctxt =
-  #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true};
+  #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt;
 
 fun cert_class ctxt class =
   let
diff -r 2df1e7bca361 -r 2028467b4df4 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Sun Mar 09 15:21:08 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Sun Mar 09 16:37:56 2014 +0100
@@ -221,7 +221,7 @@
 fun adhoc_overloading_cmd add raw_args lthy =
   let
     fun const_name ctxt =
-      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};  (* FIXME {proper = true, strict = true} (!?) *)
+      fst o dest_Const o Proof_Context.read_const {proper = false, strict = false} ctxt;  (* FIXME {proper = true, strict = true} (!?) *)
     fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
     val args =
       raw_args