eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
authorwenzelm
Tue Apr 19 21:19:14 2011 +0200 (2011-04-19)
changeset 4240605f2468d6b36
parent 42405 13ecdb3057d8
child 42407 5b9dd52f5dca
eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Apr 19 20:47:02 2011 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Apr 19 21:19:14 2011 +0200
     1.3 @@ -150,11 +150,13 @@
     1.4    let
     1.5      val vs = Term.add_vars t [];
     1.6      val fs = Term.add_frees t [];
     1.7 -  in fn 
     1.8 -      Var (ixn, _) => (case AList.lookup (op =) vs ixn of
     1.9 +  in
    1.10 +    fn Var (ixn, _) =>
    1.11 +        (case AList.lookup (op =) vs ixn of
    1.12            NONE => error "get_var_type: no such variable in term"
    1.13          | SOME T => Var (ixn, T))
    1.14 -    | Free (s, _) => (case AList.lookup (op =) fs s of
    1.15 +     | Free (s, _) =>
    1.16 +        (case AList.lookup (op =) fs s of
    1.17            NONE => error "get_var_type: no such variable in term"
    1.18          | SOME T => Free (s, T))
    1.19      | _ => error "get_var_type: not a variable"
    1.20 @@ -163,7 +165,7 @@
    1.21  fun read_term thy T s =
    1.22    let
    1.23      val ctxt = Proof_Context.init_global thy
    1.24 -      |> Proof_Syntax.strip_sorts_consttypes
    1.25 +      |> Config.put Type_Infer_Context.const_sorts false
    1.26        |> Proof_Context.set_defsort [];
    1.27      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    1.28    in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
     2.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 19 20:47:02 2011 +0200
     2.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 19 21:19:14 2011 +0200
     2.3 @@ -11,7 +11,6 @@
     2.4    val proof_of_term: theory -> bool -> term -> Proofterm.proof
     2.5    val term_of_proof: Proofterm.proof -> term
     2.6    val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
     2.7 -  val strip_sorts_consttypes: Proof.context -> Proof.context
     2.8    val read_term: theory -> bool -> typ -> string -> term
     2.9    val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
    2.10    val proof_syntax: Proofterm.proof -> theory -> theory
    2.11 @@ -201,13 +200,6 @@
    2.12      (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
    2.13    end;
    2.14  
    2.15 -fun strip_sorts_consttypes ctxt =
    2.16 -  let val {constants = (_, tab), ...} = Consts.dest (Proof_Context.consts_of ctxt)
    2.17 -  in Symtab.fold (fn (s, (T, _)) =>
    2.18 -      Proof_Context.add_const_constraint (s, SOME (Type.strip_sorts T)))
    2.19 -    tab ctxt
    2.20 -  end;
    2.21 -
    2.22  fun read_term thy topsort =
    2.23    let
    2.24      val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
    2.25 @@ -219,10 +211,7 @@
    2.26        |> Proof_Context.init_global
    2.27        |> Proof_Context.allow_dummies
    2.28        |> Proof_Context.set_mode Proof_Context.mode_schematic
    2.29 -      |> (if topsort then
    2.30 -            strip_sorts_consttypes #>
    2.31 -            Proof_Context.set_defsort []
    2.32 -          else I);
    2.33 +      |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []);
    2.34    in
    2.35      fn ty => fn s =>
    2.36        (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s