1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Sun Nov 20 16:59:37 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Nov 20 17:04:59 2011 +0100
     1.3 @@ -6,10 +6,12 @@
     1.4  
     1.5  signature QUOTIENT_DEF =
     1.6  sig
     1.7 -  val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
     1.8 +  val quotient_def:
     1.9 +    (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
    1.10      local_theory -> Quotient_Info.quotconsts * local_theory
    1.11  
    1.12 -  val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
    1.13 +  val quotient_def_cmd:
    1.14 +    (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
    1.15      local_theory -> Quotient_Info.quotconsts * local_theory
    1.16  
    1.17    val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
    1.18 @@ -85,10 +87,12 @@
    1.19  
    1.20  fun check_term' cnstr ctxt =
    1.21    Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
    1.22 -fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
    1.23 +
    1.24 +fun read_term' cnstr ctxt =
    1.25 +  check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
    1.26  
    1.27  val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
    1.28 -val quotdef_cmd = gen_quotient_def Proof_Context.read_vars read_term'
    1.29 +val quotient_def_cmd = gen_quotient_def Proof_Context.read_vars read_term'
    1.30  
    1.31  
    1.32  (* a wrapper for automatically lifting a raw constant *)
    1.33 @@ -109,6 +113,6 @@
    1.34  val _ =
    1.35    Outer_Syntax.local_theory "quotient_definition"
    1.36      "definition for constants over the quotient type"
    1.37 -      Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
    1.38 +      Keyword.thy_decl (quotdef_parser >> (snd oo quotient_def_cmd))
    1.39  
    1.40  end; (* structure *)