tuned;
authorwenzelm
Thu May 25 16:51:39 2006 +0200 (2006-05-25)
changeset 19727f5895f998402
parent 19726 df95778b4c2f
child 19728 6c47d9295dca
tuned;
src/Pure/defs.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/defs.ML	Thu May 25 16:51:37 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu May 25 16:51:39 2006 +0200
     1.3 @@ -18,8 +18,8 @@
     1.4      reducts: ((string * typ list) * (string * typ list) list) list}
     1.5    val empty: T
     1.6    val merge: Pretty.pp -> T * T -> T
     1.7 -  val define: Pretty.pp -> Consts.T ->
     1.8 -    bool -> bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
     1.9 +  val define: Pretty.pp -> bool -> bool -> string -> string ->
    1.10 +    string * typ list -> (string * typ list) list -> T -> T
    1.11  end
    1.12  
    1.13  structure Defs: DEFS =
    1.14 @@ -191,11 +191,8 @@
    1.15  
    1.16  (* define *)
    1.17  
    1.18 -fun define pp consts unchecked is_def module name lhs rhs (Defs defs) =
    1.19 +fun define pp unchecked is_def module name (c, args) deps (Defs defs) =
    1.20    let
    1.21 -    fun typargs const = (#1 const, Consts.typargs consts const);
    1.22 -    val (c, args) = typargs lhs;
    1.23 -    val deps = map typargs rhs;
    1.24      val restr =
    1.25        if plain_args args orelse
    1.26          (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
     2.1 --- a/src/Pure/theory.ML	Thu May 25 16:51:37 2006 +0200
     2.2 +++ b/src/Pure/theory.ML	Thu May 25 16:51:39 2006 +0200
     2.3 @@ -238,6 +238,9 @@
     2.4    let
     2.5      val pp = Sign.pp thy;
     2.6      val consts = Sign.consts_of thy;
     2.7 +    fun prep const =
     2.8 +      let val Const (c, T) = Sign.no_vars pp (Const const)
     2.9 +      in (c, Consts.typargs consts (c, Compress.typ thy (Type.varifyT T))) end;
    2.10  
    2.11      val lhs_vars = Term.add_tfreesT (#2 lhs) [];
    2.12      val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
    2.13 @@ -247,13 +250,7 @@
    2.14        else error ("Specification depends on extra type variables: " ^
    2.15          commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
    2.16          "\nThe error(s) above occurred in " ^ quote name);
    2.17 -
    2.18 -    fun prep const =
    2.19 -      let val Const (c, T) = Sign.no_vars pp (Const const)
    2.20 -      in (c, Compress.typ thy (Type.varifyT T)) end;
    2.21 -  in
    2.22 -    Defs.define pp consts unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs)
    2.23 -  end;
    2.24 +  in Defs.define pp unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs) end;
    2.25  
    2.26  fun add_deps a raw_lhs raw_rhs thy =
    2.27    let