# HG changeset patch
# User wenzelm
# Date 1303240754 -7200
# Node ID 05f2468d6b3624fbb74ab8e5d611a3215970460d
# Parent  13ecdb3057d8965a1fa06ecf51bd811cfa240a75
eliminated obsolete Proof_Syntax.strip_sorts_consttypes;

diff -r 13ecdb3057d8 -r 05f2468d6b36 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Apr 19 20:47:02 2011 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Apr 19 21:19:14 2011 +0200
@@ -150,11 +150,13 @@
   let
     val vs = Term.add_vars t [];
     val fs = Term.add_frees t [];
-  in fn 
-      Var (ixn, _) => (case AList.lookup (op =) vs ixn of
+  in
+    fn Var (ixn, _) =>
+        (case AList.lookup (op =) vs ixn of
           NONE => error "get_var_type: no such variable in term"
         | SOME T => Var (ixn, T))
-    | Free (s, _) => (case AList.lookup (op =) fs s of
+     | Free (s, _) =>
+        (case AList.lookup (op =) fs s of
           NONE => error "get_var_type: no such variable in term"
         | SOME T => Free (s, T))
     | _ => error "get_var_type: not a variable"
@@ -163,7 +165,7 @@
 fun read_term thy T s =
   let
     val ctxt = Proof_Context.init_global thy
-      |> Proof_Syntax.strip_sorts_consttypes
+      |> Config.put Type_Infer_Context.const_sorts false
       |> Proof_Context.set_defsort [];
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
   in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end;
diff -r 13ecdb3057d8 -r 05f2468d6b36 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 19 20:47:02 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 19 21:19:14 2011 +0200
@@ -11,7 +11,6 @@
   val proof_of_term: theory -> bool -> term -> Proofterm.proof
   val term_of_proof: Proofterm.proof -> term
   val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
-  val strip_sorts_consttypes: Proof.context -> Proof.context
   val read_term: theory -> bool -> typ -> string -> term
   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
   val proof_syntax: Proofterm.proof -> theory -> theory
@@ -201,13 +200,6 @@
     (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
   end;
 
-fun strip_sorts_consttypes ctxt =
-  let val {constants = (_, tab), ...} = Consts.dest (Proof_Context.consts_of ctxt)
-  in Symtab.fold (fn (s, (T, _)) =>
-      Proof_Context.add_const_constraint (s, SOME (Type.strip_sorts T)))
-    tab ctxt
-  end;
-
 fun read_term thy topsort =
   let
     val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy));
@@ -219,10 +211,7 @@
       |> Proof_Context.init_global
       |> Proof_Context.allow_dummies
       |> Proof_Context.set_mode Proof_Context.mode_schematic
-      |> (if topsort then
-            strip_sorts_consttypes #>
-            Proof_Context.set_defsort []
-          else I);
+      |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []);
   in
     fn ty => fn s =>
       (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s