src/Pure/type_infer_context.ML
changeset 45429 fd58cbf8cae3
parent 43278 1fbdcebb364b
child 45445 41e641a870de
     1.1 --- a/src/Pure/type_infer_context.ML	Wed Nov 09 19:01:50 2011 +0100
     1.2 +++ b/src/Pure/type_infer_context.ML	Wed Nov 09 20:47:11 2011 +0100
     1.3 @@ -259,9 +259,4 @@
     1.4      val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
     1.5    in ts' end;
     1.6  
     1.7 -val _ =
     1.8 -  Context.>>
     1.9 -    (Syntax.add_term_check 0 "standard"
    1.10 -      (fn ctxt => infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)));
    1.11 -
    1.12  end;