1.1 --- a/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 12:58:51 2014 +0100
     1.2 +++ b/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 13:44:01 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_proper ctxt false c
     1.8 +      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT 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	Thu Mar 06 12:58:51 2014 +0100
     2.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 13:44:01 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_proper ctxt false c
     2.8 +      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT 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/Datatype/rep_datatype.ML	Thu Mar 06 12:58:51 2014 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 13:44:01 2014 +0100
     3.3 @@ -534,10 +534,11 @@
     3.4          (drop (length dt_names) inducts);
     3.5  
     3.6      val ctxt = Proof_Context.init_global thy9;
     3.7 -    val case_combs = map (Proof_Context.read_const ctxt false dummyT) case_names;
     3.8 +    val case_combs =
     3.9 +      map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT) case_names;
    3.10      val constrss = map (fn (dtname, {descr, index, ...}) =>
    3.11 -      map (Proof_Context.read_const ctxt false dummyT o fst)
    3.12 -        (#3 (the (AList.lookup op = descr index)))) dt_infos
    3.13 +      map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT o fst)
    3.14 +        (#3 (the (AList.lookup op = descr index)))) dt_infos;
    3.15    in
    3.16      thy9
    3.17      |> Global_Theory.note_thmss ""

     4.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 12:58:51 2014 +0100
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 13:44:01 2014 +0100
     4.3 @@ -72,7 +72,8 @@
     4.4  val quotmaps_attribute_setup =
     4.5    Attrib.setup @{binding mapQ3}
     4.6      ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
     4.7 -      (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
     4.8 +      (Scan.lift @{keyword "("} |--
     4.9 +        Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
    4.10          Attrib.thm --| Scan.lift @{keyword ")"}) >>
    4.11        (fn (tyname, (relname, qthm)) =>
    4.12          let val minfo = {relmap = relname, quot_thm = qthm}

     5.1 --- a/src/HOL/Tools/coinduction.ML	Thu Mar 06 12:58:51 2014 +0100
     5.2 +++ b/src/HOL/Tools/coinduction.ML	Thu Mar 06 13:44:01 2014 +0100
     5.3 @@ -130,8 +130,8 @@
     5.4  
     5.5  fun rule get_type get_pred =
     5.6    named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
     5.7 -  named_rule Induct.predN (Args.const false) get_pred ||
     5.8 -  named_rule Induct.setN (Args.const false) get_pred ||
     5.9 +  named_rule Induct.predN (Args.const {proper = false, strict = false}) get_pred ||
    5.10 +  named_rule Induct.setN (Args.const {proper = false, strict = false}) get_pred ||
    5.11    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
    5.12  
    5.13  val coinduct_rule = rule Induct.lookup_coinductT Induct.lookup_coinductP >> single_rule;

     6.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 12:58:51 2014 +0100
     6.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 06 13:44:01 2014 +0100
     6.3 @@ -515,7 +515,8 @@
     6.4  val setup =
     6.5    Attrib.setup @{binding ind_realizer}
     6.6      ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
     6.7 -      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
     6.8 +      Scan.option (Scan.lift (Args.colon) |--
     6.9 +        Scan.repeat1 (Args.const {proper = false, strict = true})))) >> rlz_attrib)
    6.10      "add realizers for inductive set";
    6.11  
    6.12  end;

     7.1 --- a/src/Pure/Isar/args.ML	Thu Mar 06 12:58:51 2014 +0100
     7.2 +++ b/src/Pure/Isar/args.ML	Thu Mar 06 13:44:01 2014 +0100
     7.3 @@ -57,8 +57,7 @@
     7.4    val term_abbrev: term context_parser
     7.5    val prop: term context_parser
     7.6    val type_name: {proper: bool, strict: bool} -> string context_parser
     7.7 -  val const: bool -> string context_parser
     7.8 -  val const_proper: bool -> string context_parser
     7.9 +  val const: {proper: bool, strict: bool} -> string context_parser
    7.10    val goal_spec: ((int -> tactic) -> tactic) context_parser
    7.11    val parse: Token.T list parser
    7.12    val parse1: (string -> bool) -> Token.T list parser
    7.13 @@ -212,14 +211,10 @@
    7.14    Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
    7.15    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
    7.16  
    7.17 -fun const strict =
    7.18 -  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) strict dummyT))
    7.19 +fun const flags =
    7.20 +  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags dummyT))
    7.21    >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
    7.22  
    7.23 -fun const_proper strict =
    7.24 -  Scan.peek (fn ctxt => named_term (Proof_Context.read_const_proper (Context.proof_of ctxt) strict))
    7.25 -  >> (fn Const (c, _) => c | _ => "");
    7.26 -
    7.27  
    7.28  (* improper method arguments *)
    7.29  

     8.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 06 12:58:51 2014 +0100
     8.2 +++ b/src/Pure/Isar/proof.ML	Thu Mar 06 13:44:01 2014 +0100
     8.3 @@ -581,7 +581,7 @@
     8.4  
     8.5  val write_cmd =
     8.6    gen_write (fn ctxt => fn (c, mx) =>
     8.7 -    (Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
     8.8 +    (Proof_Context.read_const ctxt {proper = false, strict = false} (Mixfix.mixfixT mx) c, mx));
     8.9  
    8.10  end;
    8.11  

     9.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 12:58:51 2014 +0100
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 13:44:01 2014 +0100
     9.3 @@ -71,10 +71,9 @@
     9.4    val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     9.5      xstring * Position.T -> typ * Position.report list
     9.6    val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
     9.7 -  val check_const_proper: Proof.context -> bool ->
     9.8 -    xstring * Position.T -> term * Position.report list
     9.9 -  val read_const_proper: Proof.context -> bool -> string -> term
    9.10 -  val read_const: Proof.context -> bool -> typ -> string -> term
    9.11 +  val check_const: Proof.context -> {proper: bool, strict: bool} ->
    9.12 +    typ -> xstring * Position.T -> term * Position.report list
    9.13 +  val read_const: Proof.context -> {proper: bool, strict: bool} -> typ -> string -> term
    9.14    val read_arity: Proof.context -> xstring * string list * string -> arity
    9.15    val cert_arity: Proof.context -> arity -> arity
    9.16    val allow_dummies: Proof.context -> Proof.context
    9.17 @@ -470,47 +469,40 @@
    9.18  
    9.19  (* constant names *)
    9.20  
    9.21 -fun check_const_proper ctxt strict (c, pos) =
    9.22 +fun check_const ctxt {proper, strict} ty (c, pos) =
    9.23    let
    9.24      fun err msg = error (msg ^ Position.here pos);
    9.25      val consts = consts_of ctxt;
    9.26 -    val (t as Const (d, _), reports) =
    9.27 -      (case Variable.lookup_const ctxt c of
    9.28 -        SOME d =>
    9.29 +    val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
    9.30 +    val (t, reports) =
    9.31 +      (case (fixed, Variable.lookup_const ctxt c) of
    9.32 +        (SOME x, NONE) =>
    9.33            let
    9.34 -            val T = Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg;
    9.35 +            val _ = Name.reject_internal (c, [pos]);
    9.36 +            val reports =
    9.37 +              if Context_Position.is_reported ctxt pos then
    9.38 +                [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
    9.39 +              else [];
    9.40 +          in (Free (x, infer_type ctxt (x, ty)), reports) end
    9.41 +      | (_, SOME d) =>
    9.42 +          let
    9.43 +            val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
    9.44              val reports =
    9.45                if Context_Position.is_reported ctxt pos
    9.46                then [(pos, Name_Space.markup (Consts.space_of consts) d)] else [];
    9.47            in (Const (d, T), reports) end
    9.48 -      | NONE => Consts.check_const (Context.Proof ctxt) consts (c, pos));
    9.49 +      | _ => Consts.check_const (Context.Proof ctxt) consts (c, pos));
    9.50      val _ =
    9.51 -      if strict
    9.52 -      then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
    9.53 -      else ();
    9.54 +      (case (strict, t) of
    9.55 +        (true, Const (d, _)) =>
    9.56 +          (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg)
    9.57 +      | _ => ());
    9.58    in (t, reports) end;
    9.59  
    9.60 -fun read_const_proper ctxt strict text =
    9.61 +fun read_const ctxt flags ty text =
    9.62    let
    9.63      val (t, reports) =
    9.64 -      check_const_proper ctxt strict (Symbol_Pos.source_content (Syntax.read_token text));
    9.65 -    val _ = Position.reports reports;
    9.66 -  in t end;
    9.67 -
    9.68 -fun read_const ctxt strict ty text =
    9.69 -  let
    9.70 -    val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
    9.71 -    val _ = Name.reject_internal (c, [pos]);
    9.72 -    val (t, reports) =
    9.73 -      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
    9.74 -        (SOME x, false) =>
    9.75 -          let
    9.76 -            val reports =
    9.77 -              if Context_Position.is_reported ctxt pos
    9.78 -              then [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
    9.79 -              else [];
    9.80 -          in (Free (x, infer_type ctxt (x, ty)), reports) end
    9.81 -      | _ => check_const_proper ctxt strict (c, pos));
    9.82 +      check_const ctxt flags ty (Symbol_Pos.source_content (Syntax.read_token text));
    9.83      val _ = Position.reports reports;
    9.84    in t end;
    9.85  

    10.1 --- a/src/Pure/Isar/specification.ML	Thu Mar 06 12:58:51 2014 +0100
    10.2 +++ b/src/Pure/Isar/specification.ML	Thu Mar 06 13:44:01 2014 +0100
    10.3 @@ -280,7 +280,8 @@
    10.4    gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = true, strict = false});
    10.5  
    10.6  val notation = gen_notation (K I);
    10.7 -val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);
    10.8 +val notation_cmd =
    10.9 +  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false} dummyT);
   10.10  
   10.11  end;
   10.12  

    11.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 12:58:51 2014 +0100
    11.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 13:44:01 2014 +0100
    11.3 @@ -151,7 +151,7 @@
    11.4  fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
    11.5    >> (fn (ctxt, (s, pos)) =>
    11.6      let
    11.7 -      val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
    11.8 +      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT s;
    11.9        val res = check (Proof_Context.consts_of ctxt, c)
   11.10          handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   11.11      in ML_Syntax.print_string res end);
   11.12 @@ -175,7 +175,8 @@
   11.13          (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   11.14        >> (fn ((ctxt, raw_c), Ts) =>
   11.15          let
   11.16 -          val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
   11.17 +          val Const (c, _) =
   11.18 +            Proof_Context.read_const ctxt {proper = true, strict = true} dummyT raw_c;
   11.19            val consts = Proof_Context.consts_of ctxt;
   11.20            val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
   11.21            val _ = length Ts <> n andalso

    12.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:58:51 2014 +0100
    12.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 13:44:01 2014 +0100
    12.3 @@ -222,7 +222,9 @@
    12.4  (* decode_term -- transform parse tree into raw term *)
    12.5  
    12.6  fun decode_const ctxt c =
    12.7 -  let val (Const (c', _), _) = Proof_Context.check_const_proper ctxt false (c, Position.none)
    12.8 +  let
    12.9 +    val (Const (c', _), _) =
   12.10 +      Proof_Context.check_const ctxt {proper = true, strict = false} dummyT (c, Position.none);
   12.11    in c' end;
   12.12  
   12.13  fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result

    13.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 06 12:58:51 2014 +0100
    13.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Mar 06 13:44:01 2014 +0100
    13.3 @@ -573,7 +573,7 @@
    13.4    basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
    13.5    basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
    13.6    basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
    13.7 -  basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
    13.8 +  basic_entity (Binding.name "const") (Args.const {proper = true, strict = false}) pretty_const #>
    13.9    basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
   13.10    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   13.11    basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>

    14.1 --- a/src/Tools/adhoc_overloading.ML	Thu Mar 06 12:58:51 2014 +0100
    14.2 +++ b/src/Tools/adhoc_overloading.ML	Thu Mar 06 13:44:01 2014 +0100
    14.3 @@ -220,7 +220,8 @@
    14.4  
    14.5  fun adhoc_overloading_cmd add raw_args lthy =
    14.6    let
    14.7 -    fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT;
    14.8 +    fun const_name ctxt =
    14.9 +      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false} dummyT;
   14.10      fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
   14.11      val args =
   14.12        raw_args

    15.1 --- a/src/Tools/induct.ML	Thu Mar 06 12:58:51 2014 +0100
    15.2 +++ b/src/Tools/induct.ML	Thu Mar 06 13:44:01 2014 +0100
    15.3 @@ -362,8 +362,8 @@
    15.4  
    15.5  fun attrib add_type add_pred del =
    15.6    spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
    15.7 -  spec predN (Args.const false) >> add_pred ||
    15.8 -  spec setN (Args.const false) >> add_pred ||
    15.9 +  spec predN (Args.const {proper = false, strict = false}) >> add_pred ||
   15.10 +  spec setN (Args.const {proper = false, strict = false}) >> add_pred ||
   15.11    Scan.lift Args.del >> K del;
   15.12  
   15.13  in
   15.14 @@ -884,8 +884,8 @@
   15.15  
   15.16  fun rule get_type get_pred =
   15.17    named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
   15.18 -  named_rule predN (Args.const false) get_pred ||
   15.19 -  named_rule setN (Args.const false) get_pred ||
   15.20 +  named_rule predN (Args.const {proper = false, strict = false}) get_pred ||
   15.21 +  named_rule setN (Args.const {proper = false, strict = false}) get_pred ||
   15.22    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
   15.23  
   15.24  val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;

    16.1 --- a/src/Tools/subtyping.ML	Thu Mar 06 12:58:51 2014 +0100
    16.2 +++ b/src/Tools/subtyping.ML	Thu Mar 06 13:44:01 2014 +0100
    16.3 @@ -1105,7 +1105,7 @@
    16.4      (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
    16.5      "declaration of new map functions" #>
    16.6    Attrib.setup @{binding coercion_args}
    16.7 -    (Args.const false -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
    16.8 +    (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
    16.9        (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
   16.10      "declaration of new constants with coercion-invariant arguments";
   16.11