src/HOL/Tools/Quotient/quotient_def.ML
changeset 35990 5ceedb86aa9d
parent 35788 f1deaca15ca3
child 36108 03aa51cf85a2
     1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Mar 27 02:10:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Mar 27 14:48:46 2010 +0100
     1.3 @@ -12,7 +12,8 @@
     1.4    val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
     1.5      local_theory -> (term * thm) * local_theory
     1.6  
     1.7 -  val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
     1.8 +  val quotient_lift_const: typ list -> string * term -> local_theory ->
     1.9 +    (term * thm) * local_theory
    1.10  end;
    1.11  
    1.12  structure Quotient_Def: QUOTIENT_DEF =
    1.13 @@ -86,9 +87,9 @@
    1.14    quotient_def (decl, (attr, (lhs, rhs))) lthy''
    1.15  end
    1.16  
    1.17 -fun quotient_lift_const (b, t) ctxt =
    1.18 +fun quotient_lift_const qtys (b, t) ctxt =
    1.19    quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
    1.20 -    (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
    1.21 +    (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
    1.22  
    1.23  local
    1.24    structure P = OuterParse;