src/Pure/theory.ML
changeset 42394 c65c07d9967a
parent 42389 b2c6033fc7e4
child 42425 2aa907d5ee4f
     1.1 --- a/src/Pure/theory.ML	Mon Apr 18 14:05:39 2011 +0200
     1.2 +++ b/src/Pure/theory.ML	Mon Apr 18 15:01:50 2011 +0200
     1.3 @@ -240,9 +240,8 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun check_def ctxt unchecked overloaded (b, tm) defs =
     1.8 +fun check_def ctxt thy unchecked overloaded (b, tm) defs =
     1.9    let
    1.10 -    val thy = Proof_Context.theory_of ctxt;
    1.11      val name = Sign.full_name thy b;
    1.12      val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
    1.13        handle TERM (msg, _) => error msg;
    1.14 @@ -259,7 +258,7 @@
    1.15  fun add_def ctxt unchecked overloaded raw_axm thy =
    1.16    let val axm = cert_axm ctxt raw_axm in
    1.17      thy
    1.18 -    |> map_defs (check_def ctxt unchecked overloaded axm)
    1.19 +    |> map_defs (check_def ctxt thy unchecked overloaded axm)
    1.20      |> add_axiom ctxt axm
    1.21    end;
    1.22