src/Pure/Proof/extraction.ML
changeset 42406 05f2468d6b36
parent 42375 774df7c59508
child 42407 5b9dd52f5dca
     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;