recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);

--- a/src/Pure/theory.ML	Mon Apr 18 14:05:39 2011 +0200
+++ b/src/Pure/theory.ML	Mon Apr 18 15:01:50 2011 +0200
@@ -240,9 +240,8 @@
 
 local
 
-fun check_def ctxt unchecked overloaded (b, tm) defs =
+fun check_def ctxt thy unchecked overloaded (b, tm) defs =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val name = Sign.full_name thy b;
     val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
       handle TERM (msg, _) => error msg;
@@ -259,7 +258,7 @@
 fun add_def ctxt unchecked overloaded raw_axm thy =
   let val axm = cert_axm ctxt raw_axm in
     thy
-    |> map_defs (check_def ctxt unchecked overloaded axm)
+    |> map_defs (check_def ctxt thy unchecked overloaded axm)
     |> add_axiom ctxt axm
   end;