src/Pure/Tools/find_consts.ML
changeset 42360 da8817d01e7c
parent 42012 2c3fe3cbebae
child 46713 e6e1ec6d5c1c
     1.1 --- a/src/Pure/Tools/find_consts.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4    let
     1.5      val start = Timing.start ();
     1.6  
     1.7 -    val thy = ProofContext.theory_of ctxt;
     1.8 +    val thy = Proof_Context.theory_of ctxt;
     1.9      val low_ranking = 10000;
    1.10  
    1.11      fun user_visible consts (nm, _) =
    1.12 @@ -82,7 +82,7 @@
    1.13          val raw_T = Syntax.parse_typ ctxt crit;
    1.14          val t =
    1.15            Syntax.check_term
    1.16 -            (ProofContext.set_mode ProofContext.mode_pattern ctxt)
    1.17 +            (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    1.18              (Term.dummy_pattern raw_T);
    1.19        in Term.type_of t end;
    1.20