eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
authorwenzelm
Thu Mar 06 14:38:54 2014 +0100 (2014-03-06)
changeset 55955e8f1bf005661
parent 55954 a29aefc88c8d
child 55956 94d384d621b0
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
src/Doc/ProgProve/LaTeXsugar.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Tools/Datatype/rep_datatype.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/Tools/adhoc_overloading.ML
     1.1 --- a/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 13:44:01 2014 +0100
     1.2 +++ b/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 14:38:54 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} dummyT c
     1.8 +      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} 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 13:44:01 2014 +0100
     2.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 14:38:54 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} dummyT c
     2.8 +      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} 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 13:44:01 2014 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Mar 06 14:38:54 2014 +0100
     3.3 @@ -535,9 +535,9 @@
     3.4  
     3.5      val ctxt = Proof_Context.init_global thy9;
     3.6      val case_combs =
     3.7 -      map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT) case_names;
     3.8 +      map (Proof_Context.read_const ctxt {proper = false, strict = false}) case_names;
     3.9      val constrss = map (fn (dtname, {descr, index, ...}) =>
    3.10 -      map (Proof_Context.read_const ctxt {proper = false, strict = false} dummyT o fst)
    3.11 +      map (Proof_Context.read_const ctxt {proper = false, strict = false} o fst)
    3.12          (#3 (the (AList.lookup op = descr index)))) dt_infos;
    3.13    in
    3.14      thy9
     4.1 --- a/src/Pure/Isar/args.ML	Thu Mar 06 13:44:01 2014 +0100
     4.2 +++ b/src/Pure/Isar/args.ML	Thu Mar 06 14:38:54 2014 +0100
     4.3 @@ -212,7 +212,7 @@
     4.4    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
     4.5  
     4.6  fun const flags =
     4.7 -  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags dummyT))
     4.8 +  Scan.peek (fn ctxt => named_term (Proof_Context.read_const (Context.proof_of ctxt) flags))
     4.9    >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
    4.10  
    4.11  
     5.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 06 13:44:01 2014 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Thu Mar 06 14:38:54 2014 +0100
     5.3 @@ -575,13 +575,17 @@
     5.4    #> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
     5.5    #> reset_facts;
     5.6  
     5.7 +fun read_arg ctxt (c, mx) =
     5.8 +  (case Proof_Context.read_const ctxt {proper = false, strict = false} c of
     5.9 +    Free (x, _) =>
    5.10 +      let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx)
    5.11 +      in (Free (x, T), mx) end
    5.12 +  | t => (t, mx));
    5.13 +
    5.14  in
    5.15  
    5.16  val write = gen_write (K I);
    5.17 -
    5.18 -val write_cmd =
    5.19 -  gen_write (fn ctxt => fn (c, mx) =>
    5.20 -    (Proof_Context.read_const ctxt {proper = false, strict = false} (Mixfix.mixfixT mx) c, mx));
    5.21 +val write_cmd = gen_write read_arg;
    5.22  
    5.23  end;
    5.24  
     6.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 13:44:01 2014 +0100
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 14:38:54 2014 +0100
     6.3 @@ -72,8 +72,8 @@
     6.4      xstring * Position.T -> typ * Position.report list
     6.5    val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
     6.6    val check_const: Proof.context -> {proper: bool, strict: bool} ->
     6.7 -    typ -> xstring * Position.T -> term * Position.report list
     6.8 -  val read_const: Proof.context -> {proper: bool, strict: bool} -> typ -> string -> term
     6.9 +    xstring * Position.T -> term * Position.report list
    6.10 +  val read_const: Proof.context -> {proper: bool, strict: bool} -> string -> term
    6.11    val read_arity: Proof.context -> xstring * string list * string -> arity
    6.12    val cert_arity: Proof.context -> arity -> arity
    6.13    val allow_dummies: Proof.context -> Proof.context
    6.14 @@ -469,7 +469,7 @@
    6.15  
    6.16  (* constant names *)
    6.17  
    6.18 -fun check_const ctxt {proper, strict} ty (c, pos) =
    6.19 +fun check_const ctxt {proper, strict} (c, pos) =
    6.20    let
    6.21      fun err msg = error (msg ^ Position.here pos);
    6.22      val consts = consts_of ctxt;
    6.23 @@ -483,7 +483,7 @@
    6.24                if Context_Position.is_reported ctxt pos then
    6.25                  [(pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))]
    6.26                else [];
    6.27 -          in (Free (x, infer_type ctxt (x, ty)), reports) end
    6.28 +          in (Free (x, infer_type ctxt (x, dummyT)), reports) end
    6.29        | (_, SOME d) =>
    6.30            let
    6.31              val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
    6.32 @@ -499,10 +499,10 @@
    6.33        | _ => ());
    6.34    in (t, reports) end;
    6.35  
    6.36 -fun read_const ctxt flags ty text =
    6.37 +fun read_const ctxt flags text =
    6.38    let
    6.39      val (t, reports) =
    6.40 -      check_const ctxt flags ty (Symbol_Pos.source_content (Syntax.read_token text));
    6.41 +      check_const ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
    6.42      val _ = Position.reports reports;
    6.43    in t end;
    6.44  
     7.1 --- a/src/Pure/Isar/specification.ML	Thu Mar 06 13:44:01 2014 +0100
     7.2 +++ b/src/Pure/Isar/specification.ML	Thu Mar 06 14:38:54 2014 +0100
     7.3 @@ -281,7 +281,7 @@
     7.4  
     7.5  val notation = gen_notation (K I);
     7.6  val notation_cmd =
     7.7 -  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false} dummyT);
     7.8 +  gen_notation (fn ctxt => Proof_Context.read_const ctxt {proper = false, strict = false});
     7.9  
    7.10  end;
    7.11  
     8.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 13:44:01 2014 +0100
     8.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 14:38:54 2014 +0100
     8.3 @@ -151,7 +151,7 @@
     8.4  fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
     8.5    >> (fn (ctxt, (s, pos)) =>
     8.6      let
     8.7 -      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT s;
     8.8 +      val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} s;
     8.9        val res = check (Proof_Context.consts_of ctxt, c)
    8.10          handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
    8.11      in ML_Syntax.print_string res end);
    8.12 @@ -176,7 +176,7 @@
    8.13        >> (fn ((ctxt, raw_c), Ts) =>
    8.14          let
    8.15            val Const (c, _) =
    8.16 -            Proof_Context.read_const ctxt {proper = true, strict = true} dummyT raw_c;
    8.17 +            Proof_Context.read_const ctxt {proper = true, strict = true} raw_c;
    8.18            val consts = Proof_Context.consts_of ctxt;
    8.19            val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
    8.20            val _ = length Ts <> n andalso
     9.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 13:44:01 2014 +0100
     9.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 14:38:54 2014 +0100
     9.3 @@ -224,7 +224,7 @@
     9.4  fun decode_const ctxt c =
     9.5    let
     9.6      val (Const (c', _), _) =
     9.7 -      Proof_Context.check_const ctxt {proper = true, strict = false} dummyT (c, Position.none);
     9.8 +      Proof_Context.check_const ctxt {proper = true, strict = false} (c, Position.none);
     9.9    in c' end;
    9.10  
    9.11  fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
    10.1 --- a/src/Tools/adhoc_overloading.ML	Thu Mar 06 13:44:01 2014 +0100
    10.2 +++ b/src/Tools/adhoc_overloading.ML	Thu Mar 06 14:38:54 2014 +0100
    10.3 @@ -221,7 +221,7 @@
    10.4  fun adhoc_overloading_cmd add raw_args lthy =
    10.5    let
    10.6      fun const_name ctxt =
    10.7 -      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false} dummyT;
    10.8 +      fst o dest_Const o Proof_Context.read_const ctxt {proper = false, strict = false};
    10.9      fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt;
   10.10      val args =
   10.11        raw_args