src/Pure/Isar/theory_target.ML

--- a/src/Pure/Isar/theory_target.ML	Fri Aug 17 09:20:45 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Fri Aug 17 13:58:57 2007 +0200
@@ -163,7 +163,7 @@
 
 in
 
-fun defs loc kind args lthy0 =
+fun defs kind args lthy0 =
   let
     fun def ((c, mx), ((name, atts), rhs)) lthy1 =
       let
@@ -350,7 +350,7 @@
       consts = consts is_loc some_class,
       axioms = axioms,
       abbrev = abbrev is_loc some_class,
-      defs = defs loc,
+      defs = defs,
       notes = notes loc,
       type_syntax = type_syntax loc,
       term_syntax = term_syntax loc,