1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Wed Jun 29 11:58:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jun 30 10:15:46 2011 +0200
     1.3 @@ -6,10 +6,10 @@
     1.4  
     1.5  signature QUOTIENT_DEF =
     1.6  sig
     1.7 -  val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
     1.8 +  val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
     1.9      local_theory -> Quotient_Info.qconsts_info * local_theory
    1.10  
    1.11 -  val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
    1.12 +  val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
    1.13      local_theory -> Quotient_Info.qconsts_info * local_theory
    1.14  
    1.15    val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
    1.16 @@ -43,26 +43,30 @@
    1.17        quote str ^ " differs from declaration " ^ name ^ pos)
    1.18    end
    1.19  
    1.20 -fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
    1.21 +fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
    1.22    let
    1.23 +    val (vars, ctxt) = prep_vars (the_list raw_var) lthy
    1.24 +    val lhs = prep_term ctxt lhs_raw
    1.25 +    val rhs = prep_term ctxt rhs_raw
    1.26 +
    1.27      val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
    1.28      val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
    1.29      val _ = if is_Const rhs then () else warning "The definiens is not a constant"
    1.30  
    1.31 -    fun sanity_test NONE _ = true
    1.32 -      | sanity_test (SOME bind) str =
    1.33 -          if Variable.check_name bind = str then true
    1.34 -          else error_msg bind str
    1.35 +    val var =
    1.36 +      (case vars of 
    1.37 +        [] => (Binding.name lhs_str, NoSyn)
    1.38 +      | [(binding, _, mx)] =>
    1.39 +          if Variable.check_name binding = lhs_str then (binding, mx)
    1.40 +          else error_msg binding lhs_str
    1.41 +      | _ => raise Match)
    1.42  
    1.43 -    val _ = sanity_test optbind lhs_str
    1.44 -
    1.45 -    val qconst_bname = Binding.name lhs_str
    1.46      val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
    1.47      val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
    1.48      val (_, prop') = Local_Defs.cert_def lthy prop
    1.49      val (_, newrhs) = Local_Defs.abs_def prop'
    1.50  
    1.51 -    val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
    1.52 +    val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy
    1.53  
    1.54      (* data storage *)
    1.55      val qconst_data = {qconst = trm, rconst = rhs, def = thm}
    1.56 @@ -76,15 +80,9 @@
    1.57      (qconst_data, lthy'')
    1.58    end
    1.59  
    1.60 -fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
    1.61 -  let
    1.62 -    val lhs = Syntax.read_term lthy lhs_str
    1.63 -    val rhs = Syntax.read_term lthy rhs_str
    1.64 -    val lthy' = Variable.declare_term lhs lthy
    1.65 -    val lthy'' = Variable.declare_term rhs lthy'
    1.66 -  in
    1.67 -    quotient_def (decl, (attr, (lhs, rhs))) lthy''
    1.68 -  end
    1.69 +val quotient_def = gen_quotient_def Proof_Context.cert_vars Syntax.check_term
    1.70 +val quotdef_cmd = gen_quotient_def Proof_Context.read_vars Syntax.read_term
    1.71 +
    1.72  
    1.73  (* a wrapper for automatically lifting a raw constant *)
    1.74  fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
    1.75 @@ -93,14 +91,12 @@
    1.76      val qty = Quotient_Term.derive_qtyp ctxt qtys rty
    1.77      val lhs = Free (qconst_name, qty)
    1.78    in
    1.79 -    quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
    1.80 +    quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
    1.81    end
    1.82  
    1.83  (* parser and command *)
    1.84 -val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
    1.85 -
    1.86  val quotdef_parser =
    1.87 -  Scan.optional quotdef_decl (NONE, NoSyn) --
    1.88 +  Scan.option Parse_Spec.constdecl --
    1.89      Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
    1.90  
    1.91  val _ =