# HG changeset patch
# User wenzelm
# Date 1394113134 -3600
# Node ID e8f1bf005661c5462945c760d3ff145cc054438d
# Parent  a29aefc88c8db687c1c77fe4bf8bdcf2f0f9f538
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);

diff -r a29aefc88c8d -r e8f1bf005661 src/Doc/ProgProve/LaTeXsugar.thy
--- a/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 14:38:54 2014 +0100
@@ -46,7 +46,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT c
+      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} 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 a29aefc88c8d -r e8f1bf005661 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 14:38:54 2014 +0100
@@ -100,7 +100,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT c
+      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} 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 a29aefc88c8d -r e8f1bf005661 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 14:38:54 2014 +0100
@@ -535,9 +535,9 @@
 
     val ctxt = Proof_Context.init_global thy9;
     val case_combs =
-      map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT) case_names;
+      map (Proof_Context.read_const ctxt {proper = false, strict = false}) case_names;
     val constrss = map (fn (dtname, {descr, index, ...}) =>
-      map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT o fst)
+      map (Proof_Context.read_const ctxt {proper = false, strict = false} o fst)
         (#3 (the (AList.lookup op = descr index)))) dt_infos;
   in
     thy9
diff -r a29aefc88c8d -r e8f1bf005661 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Pure/Isar/args.ML	Thu Mar 06 14:38:54 2014 +0100
@@ -212,7 +212,7 @@
   >> (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 dummyT))
+  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags))
   >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
 
diff -r a29aefc88c8d -r e8f1bf005661 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Mar 06 14:38:54 2014 +0100
@@ -575,13 +575,17 @@
   #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
   #> reset_facts;
 
+fun read_arg ctxt (c, mx) =
+  (case Proof_Context.read_const ctxt {proper = false, strict = false} c of
+    Free (x, _) =>
+      let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
+      in (Free (x, T), mx) end
+  | t => (t, mx));
+
 in
 
 val write = gen_write (K I);
-
-val write_cmd =
-  gen_write (fn ctxt => fn (c, mx) =>
-    (Proof_Context.read_const ctxt {proper = false, strict = false} (Mixfix.mixfixT mx) c, mx));
+val write_cmd = gen_write read_arg;
 
 end;
 
diff -r a29aefc88c8d -r e8f1bf005661 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 14:38:54 2014 +0100
@@ -72,8 +72,8 @@
     xstring * Position.T -> typ * Position.report list
   val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
   val check_const: Proof.context -> {proper: bool, strict: bool} ->
-    typ -> xstring * Position.T -> term * Position.report list
-  val read_const: Proof.context -> {proper: bool, strict: bool} -> typ -> string -> term
+    xstring * Position.T -> term * Position.report list
+  val read_const: Proof.context -> {proper: bool, strict: bool} -> 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
@@ -469,7 +469,7 @@
 
 (* constant names *)
 
-fun check_const ctxt {proper, strict} ty (c, pos) =
+fun check_const ctxt {proper, strict} (c, pos) =
   let
     fun err msg = error (msg ^ Position.here pos);
     val consts = consts_of ctxt;
@@ -483,7 +483,7 @@
               if Context_Position.is_reported ctxt pos then
                 [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
               else [];
-          in (Free (x, infer_type ctxt (x, ty)), reports) end
+          in (Free (x, infer_type ctxt (x, dummyT)), reports) end
       | (_, SOME d) =>
           let
             val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
@@ -499,10 +499,10 @@
       | _ => ());
   in (t, reports) end;
 
-fun read_const ctxt flags ty text =
+fun read_const ctxt flags text =
   let
     val (t, reports) =
-      check_const ctxt flags ty (Symbol_Pos.source_content (Syntax.read_token text));
+      check_const ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
     val _ = Position.reports reports;
   in t end;
 
diff -r a29aefc88c8d -r e8f1bf005661 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 06 14:38:54 2014 +0100
@@ -281,7 +281,7 @@
 
 val notation = gen_notation (K I);
 val notation_cmd =
-  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false} dummyT);
+  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false});
 
 end;
 
diff -r a29aefc88c8d -r e8f1bf005661 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 14:38:54 2014 +0100
@@ -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} dummyT s;
+      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} 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} dummyT raw_c;
+            Proof_Context.read_const ctxt {proper = true, strict = true} 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 a29aefc88c8d -r e8f1bf005661 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 14:38:54 2014 +0100
@@ -224,7 +224,7 @@
 fun decode_const ctxt c =
   let
     val (Const (c', _), _) =
-      Proof_Context.check_const ctxt {proper = true, strict = false} dummyT (c, Position.none);
+      Proof_Context.check_const ctxt {proper = true, strict = false} (c, Position.none);
   in c' end;
 
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
diff -r a29aefc88c8d -r e8f1bf005661 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Thu Mar 06 13:44:01 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Thu Mar 06 14:38:54 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} dummyT;
+      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};
     fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
     val args =
       raw_args