src/Pure/theory.ML
changeset 19727 f5895f998402
parent 19708 a508bde37a81
child 19806 f860b7a98445
     1.1 --- a/src/Pure/theory.ML	Thu May 25 16:51:37 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu May 25 16:51:39 2006 +0200
     1.3 @@ -238,6 +238,9 @@
     1.4    let
     1.5      val pp = Sign.pp thy;
     1.6      val consts = Sign.consts_of thy;
     1.7 +    fun prep const =
     1.8 +      let val Const (c, T) = Sign.no_vars pp (Const const)
     1.9 +      in (c, Consts.typargs consts (c, Compress.typ thy (Type.varifyT T))) end;
    1.10  
    1.11      val lhs_vars = Term.add_tfreesT (#2 lhs) [];
    1.12      val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
    1.13 @@ -247,13 +250,7 @@
    1.14        else error ("Specification depends on extra type variables: " ^
    1.15          commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
    1.16          "\nThe error(s) above occurred in " ^ quote name);
    1.17 -
    1.18 -    fun prep const =
    1.19 -      let val Const (c, T) = Sign.no_vars pp (Const const)
    1.20 -      in (c, Compress.typ thy (Type.varifyT T)) end;
    1.21 -  in
    1.22 -    Defs.define pp consts unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs)
    1.23 -  end;
    1.24 +  in Defs.define pp unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs) end;
    1.25  
    1.26  fun add_deps a raw_lhs raw_rhs thy =
    1.27    let