src/Pure/theory.ML
changeset 24981 4ec3f95190bf
parent 24966 70111480b84b
child 25017 e82ab4962f80
     1.1 --- a/src/Pure/theory.ML	Thu Oct 11 19:10:22 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Oct 11 19:10:23 2007 +0200
     1.3 @@ -294,8 +294,9 @@
     1.4  
     1.5  fun check_def thy unchecked overloaded (bname, tm) defs =
     1.6    let
     1.7 +    val ctxt = ProofContext.init thy;
     1.8      val name = Sign.full_name thy bname;
     1.9 -    val (lhs_const, rhs) = Sign.cert_def (Sign.pp thy) tm;
    1.10 +    val (lhs_const, rhs) = Sign.cert_def ctxt tm;
    1.11      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
    1.12      val _ = check_overloading thy overloaded lhs_const;
    1.13    in defs |> dependencies thy unchecked true name lhs_const rhs_consts end