# HG changeset patch
# User wenzelm
# Date 1394109841 -3600
# Node ID a29aefc88c8db687c1c77fe4bf8bdcf2f0f9f538
# Parent  b19373bd7ea85f7f8937ad1101c688b52620d353
more uniform check_const/read_const;

diff -r b19373bd7ea8 -r a29aefc88c8d src/Doc/ProgProve/LaTeXsugar.thy
--- a/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 13:44:01 2014 +0100
@@ -46,7 +46,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const_proper ctxt false c
+      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT 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 b19373bd7ea8 -r a29aefc88c8d src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 13:44:01 2014 +0100
@@ -100,7 +100,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const_proper ctxt false c
+      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT 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 b19373bd7ea8 -r a29aefc88c8d src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -534,10 +534,11 @@
         (drop (length dt_names) inducts);
 
     val ctxt = Proof_Context.init_global thy9;
-    val case_combs = map (Proof_Context.read_const ctxt false dummyT) case_names;
+    val case_combs =
+      map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT) case_names;
     val constrss = map (fn (dtname, {descr, index, ...}) =>
-      map (Proof_Context.read_const ctxt false dummyT o fst)
-        (#3 (the (AList.lookup op = descr index)))) dt_infos
+      map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT o fst)
+        (#3 (the (AList.lookup op = descr index)))) dt_infos;
   in
     thy9
     |> Global_Theory.note_thmss ""
diff -r b19373bd7ea8 -r a29aefc88c8d src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -72,7 +72,8 @@
 val quotmaps_attribute_setup =
   Attrib.setup @{binding mapQ3}
     ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
-      (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
+      (Scan.lift @{keyword "("} |--
+        Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
         Attrib.thm --| Scan.lift @{keyword ")"}) >>
       (fn (tyname, (relname, qthm)) =>
         let val minfo = {relmap = relname, quot_thm = qthm}
diff -r b19373bd7ea8 -r a29aefc88c8d src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -130,8 +130,8 @@
 
 fun rule get_type get_pred =
   named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
-  named_rule Induct.predN (Args.const false) get_pred ||
-  named_rule Induct.setN (Args.const false) get_pred ||
+  named_rule Induct.predN (Args.const {proper = false, strict = false}) get_pred ||
+  named_rule Induct.setN (Args.const {proper = false, strict = false}) get_pred ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
 
 val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;
diff -r b19373bd7ea8 -r a29aefc88c8d src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -515,7 +515,8 @@
 val setup =
   Attrib.setup @{binding ind_realizer}
     ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
-      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
+      Scan.option (Scan.lift (Args.colon) |--
+        Scan.repeat1 (Args.const {proper = false, strict = true})))) >> rlz_attrib)
     "add realizers for inductive set";
 
 end;
diff -r b19373bd7ea8 -r a29aefc88c8d src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/Isar/args.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -57,8 +57,7 @@
   val term_abbrev: term context_parser
   val prop: term context_parser
   val type_name: {proper: bool, strict: bool} -> string context_parser
-  val const: bool -> string context_parser
-  val const_proper: bool -> string context_parser
+  val const: {proper: bool, strict: bool} -> string context_parser
   val goal_spec: ((int -> tactic) -> tactic) context_parser
   val parse: Token.T list parser
   val parse1: (string -> bool) -> Token.T list parser
@@ -212,14 +211,10 @@
   Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
   >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
-fun const strict =
-  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) strict dummyT))
+fun const flags =
+  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags dummyT))
   >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
-fun const_proper strict =
-  Scan.peek (fn ctxt => named_term (Proof_Context.read_const_proper (Context.proof_of ctxt) strict))
-  >> (fn Const (c, _) => c | _ => "");
-
 
 (* improper method arguments *)
 
diff -r b19373bd7ea8 -r a29aefc88c8d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -581,7 +581,7 @@
 
 val write_cmd =
   gen_write (fn ctxt => fn (c, mx) =>
-    (Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
+    (Proof_Context.read_const ctxt {proper = false, strict = false} (Mixfix.mixfixT mx) c, mx));
 
 end;
 
diff -r b19373bd7ea8 -r a29aefc88c8d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -71,10 +71,9 @@
   val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     xstring * Position.T -> typ * Position.report list
   val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
-  val check_const_proper: Proof.context -> bool ->
-    xstring * Position.T -> term * Position.report list
-  val read_const_proper: Proof.context -> bool -> string -> term
-  val read_const: Proof.context -> bool -> typ -> string -> term
+  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
   val read_arity: Proof.context -> xstring * string list * string -> arity
   val cert_arity: Proof.context -> arity -> arity
   val allow_dummies: Proof.context -> Proof.context
@@ -470,47 +469,40 @@
 
 (* constant names *)
 
-fun check_const_proper ctxt strict (c, pos) =
+fun check_const ctxt {proper, strict} ty (c, pos) =
   let
     fun err msg = error (msg ^ Position.here pos);
     val consts = consts_of ctxt;
-    val (t as Const (d, _), reports) =
-      (case Variable.lookup_const ctxt c of
-        SOME d =>
+    val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
+    val (t, reports) =
+      (case (fixed, Variable.lookup_const ctxt c) of
+        (SOME x, NONE) =>
           let
-            val T = Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg;
+            val _ = Name.reject_internal (c, [pos]);
+            val reports =
+              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
+      | (_, SOME d) =>
+          let
+            val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
             val reports =
               if Context_Position.is_reported ctxt pos
               then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
           in (Const (d, T), reports) end
-      | NONE => Consts.check_const (Context.Proof ctxt) consts (c, pos));
+      | _ => Consts.check_const (Context.Proof ctxt) consts (c, pos));
     val _ =
-      if strict
-      then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
-      else ();
+      (case (strict, t) of
+        (true, Const (d, _)) =>
+          (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg)
+      | _ => ());
   in (t, reports) end;
 
-fun read_const_proper ctxt strict text =
+fun read_const ctxt flags ty text =
   let
     val (t, reports) =
-      check_const_proper ctxt strict (Symbol_Pos.source_content (Syntax.read_token text));
-    val _ = Position.reports reports;
-  in t end;
-
-fun read_const ctxt strict ty text =
-  let
-    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
-    val _ = Name.reject_internal (c, [pos]);
-    val (t, reports) =
-      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
-        (SOME x, false) =>
-          let
-            val reports =
-              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
-      | _ => check_const_proper ctxt strict (c, pos));
+      check_const ctxt flags ty (Symbol_Pos.source_content (Syntax.read_token text));
     val _ = Position.reports reports;
   in t end;
 
diff -r b19373bd7ea8 -r a29aefc88c8d src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -280,7 +280,8 @@
   gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = true, strict = false});
 
 val notation = gen_notation (K I);
-val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);
+val notation_cmd =
+  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false} dummyT);
 
 end;
 
diff -r b19373bd7ea8 -r a29aefc88c8d src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 13:44:01 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_proper ctxt false s;
+      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT 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);
@@ -175,7 +175,8 @@
         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
       >> (fn ((ctxt, raw_c), Ts) =>
         let
-          val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
+          val Const (c, _) =
+            Proof_Context.read_const ctxt {proper = true, strict = true} dummyT 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 b19373bd7ea8 -r a29aefc88c8d src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -222,7 +222,9 @@
 (* decode_term -- transform parse tree into raw term *)
 
 fun decode_const ctxt c =
-  let val (Const (c', _), _) = Proof_Context.check_const_proper ctxt false (c, Position.none)
+  let
+    val (Const (c', _), _) =
+      Proof_Context.check_const ctxt {proper = true, strict = false} dummyT (c, Position.none);
   in c' end;
 
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
diff -r b19373bd7ea8 -r a29aefc88c8d src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -573,7 +573,7 @@
   basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
   basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
   basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
-  basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
+  basic_entity (Binding.name "const") (Args.const {proper = true, strict = false}) pretty_const #>
   basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
   basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
diff -r b19373bd7ea8 -r a29aefc88c8d src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -220,7 +220,8 @@
 
 fun adhoc_overloading_cmd add raw_args lthy =
   let
-    fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT;
+    fun const_name ctxt =
+      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false} dummyT;
     fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
     val args =
       raw_args
diff -r b19373bd7ea8 -r a29aefc88c8d src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Tools/induct.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -362,8 +362,8 @@
 
 fun attrib add_type add_pred del =
   spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
-  spec predN (Args.const false) >> add_pred ||
-  spec setN (Args.const false) >> add_pred ||
+  spec predN (Args.const {proper = false, strict = false}) >> add_pred ||
+  spec setN (Args.const {proper = false, strict = false}) >> add_pred ||
   Scan.lift Args.del >> K del;
 
 in
@@ -884,8 +884,8 @@
 
 fun rule get_type get_pred =
   named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
-  named_rule predN (Args.const false) get_pred ||
-  named_rule setN (Args.const false) get_pred ||
+  named_rule predN (Args.const {proper = false, strict = false}) get_pred ||
+  named_rule setN (Args.const {proper = false, strict = false}) get_pred ||
   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
 
 val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;
diff -r b19373bd7ea8 -r a29aefc88c8d src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Tools/subtyping.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -1105,7 +1105,7 @@
     (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
     "declaration of new map functions" #>
   Attrib.setup @{binding coercion_args}
-    (Args.const false -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
+    (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
       (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
     "declaration of new constants with coercion-invariant arguments";