--- a/src/Pure/theory.ML Thu Aug 09 15:52:53 2007 +0200
+++ b/src/Pure/theory.ML Thu Aug 09 15:52:54 2007 +0200
@@ -214,7 +214,7 @@
else error ("Specification depends on extra type variables: " ^
commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
"\nThe error(s) above occurred in " ^ quote name);
- in Defs.define pp unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs) end;
+ in Defs.define pp unchecked is_def name (prep lhs) (map prep rhs) end;
fun add_deps a raw_lhs raw_rhs thy =
let