src/Pure/Isar/local_defs.ML
changeset 24961 5298ee9c3fe5
parent 24261 dd31811bdf46
child 24981 4ec3f95190bf
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Oct 11 16:05:26 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Oct 11 16:05:30 2007 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  
     1.5  fun cert_def ctxt eq =
     1.6    let
     1.7 -    val pp = ProofContext.pp ctxt;
     1.8 +    val pp = Syntax.pp ctxt;
     1.9      val display_term = quote o Pretty.string_of_term pp;
    1.10      fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
    1.11      val ((lhs, _), eq') = eq