--- 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;