src/Pure/theory.ML
changeset 24199 8be734b5f59f
parent 24137 8d7896398147
child 24626 85eceef2edc7
     1.1 --- a/src/Pure/theory.ML	Thu Aug 09 15:52:53 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Aug 09 15:52:54 2007 +0200
     1.3 @@ -214,7 +214,7 @@
     1.4        else error ("Specification depends on extra type variables: " ^
     1.5          commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
     1.6          "\nThe error(s) above occurred in " ^ quote name);
     1.7 -  in Defs.define pp unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs) end;
     1.8 +  in Defs.define pp unchecked is_def name (prep lhs) (map prep rhs) end;
     1.9  
    1.10  fun add_deps a raw_lhs raw_rhs thy =
    1.11    let